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...
Simplify some uses of `pr_global_env` by using `Termops.pr_global_env`.
And: - coqdoc.py is rocqdoc.py - coqtop.py is rocqtop.py Many other renamings, all related to doc generation. `doc/tools/` is now mostly free of 'coq|Coq|COQ'. Some were not possible at this...
I would be happy to have some attribute to control in which Coq versions some commands are executed in the spirit of a preprocessor directive. This could help in particular...
This goes surprisingly well in stdlib. Let's see what the bench says.
interp_notation_as_global_reference_expanded returns the scope name, gotten from the key in the scope map. When checking a specific scope (`About "foo"%bar`) it is specified using it delimiter, and we would produce...
Manual fixes: the well-parenthesized "match!" notations go at level 0, now is at level 1 with arg at level 6. Autodetect simple heuristic: - starts with ident (or ident-like keyword):...
### Description of the problem The bench doesn't work for PRs having overlays. It should be possible to inspect the overlay files and pin the opam packages to the overlay...
About print `(* mutable *)` after the type. Print also prints modules which mutated the value (like Ltac1).
Fixes / closes #20779 This fixes an issue with the resolution of canonical structures in presence of univ poly that did not register the right typing constraints. I'm not sure...