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...
### Is your feature request related to a problem? In classes, it is often the case that we want to show multiple proofs of the same lemma. At this point,...
The goal is to be able to detect bugs like https://github.com/coq/coq/issues/20224 so we don't want to just check that all templates are fully applied. Instead we keep around a set...
VERNAC EXTEND doc should be reasonably complete with this. We could also consider promoting parsing.md to a refman page.
### Description of the problem I think there is an issue with the reverse coercion mechanism. Take: - `A1` (reverse) coercible to class `C` through class `B`, with the coercion...
Depends: - https://github.com/rocq-prover/rocq/pull/20542
Errors: ``` logs/primitive/arrays/get.v.log ==========> TESTING primitive/arrays/get.v t.[0] : forall A : Type, array A -> A fun (A : Type) (t : array A) => t.[0] : forall A :...
If: - coercion class `A1` is (reverse) coercible to class `C` through class `B`, with the coercion between `A1` and `B` an identity coercion `id_A1`; - coercion class `A2` is...
### Description of the problem ``` COQPATH=$PWD rocq repl -w -deprecated-coq-env-var Warning, feedback message received but no listener to handle it! Warning, feedback message received but no listener to handle...
The PR makes a minimal modification to the proof-search of `tauto` so that `axioms` are checked for each time a new formula is generated. + This may avoid performing a...
### Description of the problem The `Combined Scheme` is very inconsistent and sometimes crashes. Several examples: ```coq Inductive A := a : A with B := b : B. Scheme...
