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...
### Description of the problem When enclosing abbreviations in a module B, importing outer modules (e.g. A) will make the abbreviation printed, even when not importing module B. This is...
### Description of the problem When Type-in-Type is set, sort unification discards quality equalities, leading to wrong relevance marks, which errors in the end. ### Small Rocq / Coq file...
### Is your feature request related to a problem? Because `Cumulative` sort polymorphic records are not cumulative in sorts, this code fails: ```coq #[export] Set Universe Polymorphism. #[export] Set Polymorphic...
For experimentation I set to to require exact substring match when the searched string has length
### Description of the problem Definitional UIP does not reduce proofs of `seq A1 A2` to `srefl` when `A1` and `A2` differ only in (unifiable) universe levels, which significantly inhibits...
Fixes / closes #???? [#Rocq users > Set Printing FullyQualifiedNames. @ 💬](https://rocq-prover.zulipchat.com/#narrow/channel/237977-Rocq-users/topic/Set.20Printing.20FullyQualifiedNames.2E/near/516341091) - [ ] Added / updated **test-suite**. - [ ] Added **changelog**. - [ ] Added / updated...
### Description of the problem It seems lia reduces `pow` functions on constant arguments in a very inefficient way. Reducing the exponent by one order of magnitude makes the examples...
#### Description of the problem Don't know if this is a real bug or a feature. In the latter case I would like to ask for a workaround. `specialize` does...
#### Description of the problem The following proof script worked fine in Coq 8.13 and 8.14, but stopped working with 8.15: ``` Lemma test (X : nat -> Prop) (H...
