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...
This will allow splitting tac2intern more, for instance have pattern analysis in its own file.
The proof mode for the current proof was handled by the STM. We move this piece of state in Pvernac and include it into Vernacstate.Parser.t so that "the parsing state"...
It occurs to me that the loadpath shown by `Print LoadPath` would be much easier to read if it was sorted by logical name (possibly case-insensitive), provided it preserves the...
**Kind:** bug fix Fixes / closes #9412 This is a quick fix (which will have to be adapted on top of #12272). - [X] Added / updated test-suite - [X]...
#### Description of the problem The following code: ```coq Reserved Notation "\[]" (at level 0). Class hoare (heap : Type) := { hempty : heap -> Prop := fun h...
- https://github.com/math-comp/math-comp/pull/911 Embeds #16366 #16367
With the `using` attribute one can make sure that a `Definition` is generalized over a section variable regardless of whether it is used. For example: ```coq Section foo. Context (a...
There is a way to print keywords from coqtop.byte, but not from coqtop / coqc. I cannot seem to run `coqtop.byte`, as I get ``` Fatal error: cannot load shared...
We turn the Hint locality warning into an error. - close https://github.com/coq/coq/issues/13394 - [ ] improve warning message? - [ ] documentation Depends on: - [x] https://github.com/coq/coq/pull/16251 Closed PRs are...
