GGaëtan GilbertRemove more global lazys
| 文件 | 最后提交记录 | 最后更新时间 |
|---|---|---|
Remove compat coq-core libraries (not executables) Keep coq-core.kernel because it's used by dune coq mode. | 4 个月前 | |
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 个月前 | |
Stop relying on atoms to discriminate goal formulas in firstorder. | 1 年前 | |
Remove more global lazys | 3 个月前 | |
Rename the Pcoq module into Procq. | 1 年前 | |
Deprecate Tacmach.pf_env. | 9 个月前 | |
Clean up the Firstorder implementation. We remove dead code that was there to handle the now defunct gintuition. | 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 个月前 | |
Update the OCaml headers to reflect the fact Coq is now Rocq. This was generated with a sed script applied to all files with extensions {ml, mli, mly, mll, mlg}. | 1 年前 | |
Stop opening Tacmach module and qualify uses instead. | 9 个月前 | |
Do not store the domain pattern in left-hand-side firstorder arrow pattern. | 1 年前 | |
Stop relying on atoms to discriminate goal formulas in firstorder. | 1 年前 | |
Stop keeping track of hypotheses in a dedicated firstorder context. After the previous commit this is dead code. | 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 个月前 | |
Use a fast path in Unify.unify_atom. There is no point in trying to unify two terms to find the value of a meta if it does not appear in any of these terms. We have to be a bit careful because the caller may make a difference between the None and the Some Phantom case depending on the phref value, so we pass this as an additional boolean flag. | 1 年前 |