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...
Unifying structures is very slow (see e.g. https://github.com/math-comp/math-comp/pull/1365). So whenever we see a projection, we can try to reduce it. This also simplifies the Canonical Structures procedure (e.g. gets rid...
### Description of the problem In the following example, `destruct` names the argument to constructor `s` variable `s`. So, when the environment and the list of allowed variables get printed,...
### Description of the problem I was trying to answer this question [1] and I removed the *Program* keyword but then I got the following error message: Anomaly "in econstr:...
Follows PR #19537 and #18903. Currently all squashed in a single commit, to be reorganized in many different PRs, when possible. This is mainly to make it easily available for...
### Description of the problem `man rocq` does not list the subcommands and provides a wrong URL. ``` ROCQ(1) General Commands Manual ROCQ(1) NAME rocq - The Rocq Prover SYNOPSIS...
### Description of the problem More generally, mutual (co-)fixpoints that share names are not properly taken into account. - `fix f ... with f ... as f` is accepted, but...
### Description of the problem When querying a notation in a scope with Print and About, there is an error for both scope options. In repl : ``` Rocq <...
Overlays: - https://github.com/ejgallego/coq-lsp/pull/982
Until now, the algorithm unfolded terms blindly and instantiated an evar with whatever term was on the other side. Now, we remember the terms from the initial unification problem, and...
also Ccnv Profiling