GGaëtan GilbertRemove compat coq-core libraries (not executables)
| 文件 | 最后提交记录 | 最后更新时间 |
|---|---|---|
Remove compat coq-core libraries (not executables) Keep coq-core.kernel because it's used by dune coq mode. | 3 个月前 | |
Split some primitive notation code from notation.ml Some is still in notation.ml because it deals with scopes and synchronized state. | 1 年前 | |
Rename the Pcoq module into Procq. | 1 年前 | |
Move the dubious compare and hash functions from Constr to a Termops submodule. These functions make very little sense in general as they mostly ignore most invariants about terms. They are only used by plugins and thankfully never in the kernel. Their main use seems to treat constr as a first-order data type with an otherwise unspecified representation. | 5 个月前 | |
Split some primitive notation code from notation.ml Some is still in notation.ml because it deals with scopes and synchronized state. | 1 年前 |