PPierre-Marie PédrotAbstract away the Summary reference type.
| 文件 | 最后提交记录 | 最后更新时间 |
|---|---|---|
Fixing typos - Part 2 | 7 年前 | |
Rename Coq -> Rocq in various comments and doc Co-authored-by: Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> Co-authored-by: Guillaume Melquiond <guillaume.melquiond@inria.fr> | 1 年前 | |
Fix #22229 (Extraction use "Rocq" prefix instead of "Coq") Fixes https://github.com/rocq-prover/rocq/issues/22229 | 1 个月前 | |
Deprecate Names.Label This opaque alias of Id does not seem useful and mostly results in sprinkling Label.to/of_id around the codebase. Close #21102 | 10 个月前 | |
Remove compat coq-core libraries (not executables) Keep coq-core.kernel because it's used by dune coq mode. | 3 个月前 | |
Merge PR #22354: Fix extraction on sort poly constant Reviewed-by: ppedrot Co-authored-by: ppedrot <ppedrot@users.noreply.github.com> | 24 天前 | |
Use a dedicated type for globals in extraction. | 1 年前 | |
Merge PR #22349: Fix singleton extraction after implicit erasure Reviewed-by: ppedrot Co-authored-by: ppedrot <ppedrot@users.noreply.github.com> | 12 天前 | |
Monomorphize sort-polymorphic definitions in extraction. | 1 年前 | |
rename package coq-core -> rocq-runtime | 1 年前 | |
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 年前 | |
More precise typing for module file extraction table. | 1 年前 | |
Introduce a wrapper around the Table.t type in extraction. For now this is semantically the identity but it will allow keeping a read-only state on the side. | 1 年前 | |
More precise typing for module file extraction table. | 1 年前 | |
Introduce a wrapper around the Table.t type in extraction. For now this is semantically the identity but it will allow keeping a read-only state on the side. | 1 年前 | |
QGlobal is not QVar | 5 个月前 | |
Deprecate Names.Label This opaque alias of Id does not seem useful and mostly results in sprinkling Label.to/of_id around the codebase. Close #21102 | 10 个月前 | |
Deprecate Names.Label This opaque alias of Id does not seem useful and mostly results in sprinkling Label.to/of_id around the codebase. Close #21102 | 10 个月前 | |
Use a dedicated type for globals in extraction. | 1 年前 | |
Fix duplicate constant in extraction warnings when sort poly | 26 天前 | |
Use a dedicated type for globals in extraction. | 1 年前 | |
Patch for issue #21176. Extraction now handles 'effect' keyword in OCaml 5.3.0 and higher. | 9 个月前 | |
Introduce a wrapper around the Table.t type in extraction. For now this is semantically the identity but it will allow keeping a read-only state on the side. | 1 年前 | |
Centralize the visibility extraction state in State.t. This is a bit more tricky than the previous states, because this precise bit of data follows a reader-like discipline rather than a purely state-passing one. We have to mess a bit with the exposed APIs to make this clear. | 1 年前 | |
Introduce a wrapper around the Table.t type in extraction. For now this is semantically the identity but it will allow keeping a read-only state on the side. | 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. | 24 天前 | |
Merge PR #22355: Fix opaque accessing extraction of opaque sort poly constant Reviewed-by: ppedrot Co-authored-by: ppedrot <ppedrot@users.noreply.github.com> | 25 天前 |