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...
After this AFAICT the only global universes still using raw ints are the ones from module types (because the name object doesn't escape) - fix collision with generated names -...
When set, the list of hypotheses needed by lia,nia,lra,nra proofs are printed. It should be safe to clear them and therefore speed-up proof search. - [x] Added **changelog**. - [...
The items listed under "For XXX ->" were sorted using `GlobRef.UserOrd`, which IINM sorts first on the type (VarRef, ConstRef, IndRef or ConstructRef) and then alphabetically. Since the output doesn't...
### Description of the problem In the following example, I expected the definition to work, instead of failing with a type class error. The type classes can be properly inferred...
Fixes / closes #19658 - [x] Added / updated **test-suite**. - [x] Added **changelog**. - ~[ ] Added / updated **documentation**.~ - ~[ ] Documented any new / changed **user...
Now `Fin.case_L_R'` and `Fin.case_L_R` can be used in computation, similarly to `Fin.caseS'` and `Fin.caseS`. Added lemmas `Fin.case_L_R'_L`, `Fin.case_L_R'_R`, `Fin.case_L_R_L`, `Fin.case_L_R_R`, which are now provable. - [x] Added **changelog**.
This is a first step to implements part of [CEP#83](https://github.com/coq/ceps/pull/83) that reached a common agreement during the dedicated Coq call discussions (tl;dr: give stdlib its own repository, clarify its internal...
Fixes / closes #19541 - [x] Added / updated **test-suite**. - [x] Added **changelog**. - ~[ ] Added / updated **documentation**.~ - ~[ ] Documented any new / changed **user...