Pierre Roux
Pierre Roux
##### Motivation for this change Many lemmas for bigops on monoids (particularly abelian ones) were already valid on (abelian) semigroups. This generalization could be improved by adding semigroups to the...
``` Warning: The default value for rewriting hint locality is currently "local" in a section and "global" otherwise, but is scheduled to change in a future release. For the time...
To be able to use PG with `emacs -nw`, I need to add the following line to my `.emacs` ``` (setq overlay-arrow-string nil) ``` otherwise a useless arrow `=>` hides...
The new ssreflect's `under` tactic https://coq.inria.fr/distrib/current/refman/proof-engine/ssreflect-proof-language.html?highlight=under#rewriting-under-binders lacks some syntax highlighting and indentation support.
Fixes #550 Classical currently contains boolp and classical_sets, we may also consider adding functions and signed there.
Just for the CI on math-comp/math-comp#733 to go through on coq master (this is just a merge commit).
Should the following issue a warning? ``` HB.export RealDomainExports. HB.export RealDomainExports. (*
Just to remember we have that branch.