PPierre-Marie PédrotAbstract away the Summary reference type.
| 文件 | 最后提交记录 | 最后更新时间 |
|---|---|---|
Remove compat coq-core libraries (not executables) Keep coq-core.kernel because it's used by dune coq mode. | 3 个月前 | |
Rename is_section_variable' -> is_section_variable_env | 3 个月前 | |
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 年前 | |
Keep track of variable status (secvar or not) in named contexts Close #6773 | 3 个月前 | |
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 年前 | |
QGlobal is not QVar | 5 个月前 | |
Use of QualityOrSet in elimination scheme generation | 1 年前 | |
Implement `{| foo with fields |}` for terms Fix #14438 Co-authored-by: Clément Pit-Claudel <cpitclaudel@users.noreply.github.com> | 2 个月前 | |
Use of QualityOrSet in elimination scheme generation | 1 年前 | |
Keep track of variable status (secvar or not) in named contexts Close #6773 | 3 个月前 | |
[ocamlformat] Enable for funind. As part of the proof refactoring work I am doing some modifications to `funind` and indentation of that code is driving me a bit crazy; I'd much prefer to delegate it to an automatic tool. | 6 年前 | |
Use variable status to decide if a variable is section variable Termops.is_section_variable is deprecated and a new API Termops.is_section_variable' is added because their types are the same but they need different env arguments so changing in place would be too footgunny. ssr still uses the old "is it in global env" because IDK what it is doing. Fix #18858 | 3 个月前 | |
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 年前 | |
Reduce the exposure of QualityOrSet.t type in the Retyping API. This horrendous type should never have escaped from its very specific use-case, namely to be able to have separate induction principles for predicates returning a Set or a Type. We expose a proper retyping primitive giving direct access to the quality, which is what most users actually rely on. | 3 个月前 | |
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 年前 | |
Abstract away the Summary reference type. There is no reason to expose this type as the usual OCaml reference type, and doing so prevents experimenting with more clever implementations where the liboject internals can track the references in a different way. | 21 天前 | |
Stop using global lazy in funind | 3 个月前 | |
Remove the not extremely well-named Inv.inv function. It was only used once in funind and the function is easily reachable through the Inv.inv_clause wrapper. | 6 个月前 | |
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 年前 | |
Keep track of variable status (secvar or not) in named contexts Close #6773 | 3 个月前 | |
[declare] Move proof information to declare. At this point the record in lemmas was just a stub; next commit will stop exposing the internals of mutual information, and pave the way for the refactoring of `Info.t` handling in the Declare interface. | 6 年前 |