coq
coq copied to clipboard
coq
Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive developme...
Fix #10816 depends - https://github.com/coq/coq/pull/19016 Overlays: - https://github.com/HoTT/Coq-HoTT/pull/1958 (backwards compatible) - https://github.com/mattam82/Coq-Equations/pull/594 (backwards compatible)
Close #3132 (although maybe we should open a similar issue for Scheme Equality?)
This is a series of cleanups that make the VM and native generate the same lambda code up to structured values. Apart for the simple cleanups, the VM pipeline is...
This makes a step in direction to have gramlib respecting the choice of non-associativity and the choice of levels made by the user. The PR adds internal flags to activate...
Rather than folding over the list, which is repeatingly mapping over the whole term, we map once over the term and perform the substitution of constants there. Most of the...
Continuation of https://github.com/coq/coq/pull/18890
17 years after the first version of `Program`, this PR debugs the (anticipated) support for multiple patterns involving inductive families. By fixing several de Bruijn indexes bugs, by detecting heteregeneous...
Follow-up to https://github.com/coq/coq/pull/18890 Not sure what the effect on this will be, doing as suggested by the PR discussion.
Close #11118 This PR proposes a simpler workaround than PR https://github.com/coq/coq/pull/11200. Cc @gares @CohenCyril @proux01 @mrhaandi FYI - [x] Added / updated **test-suite**. - [x] Added **changelog**. - [x] Added...
~~~coq Require Import Program.Tactics. Set Universe Polymorphism. (* needed because we don't enforce universe declarations on obligations, in univ poly mode however the universes must be redeclared for the main...