| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
|
|
This gives user control on the transparent state of a hint db. Can
override defaults more easily (report by J. H. Jourdan).
For "core", declare that variables can be unfolded, but no constants
(ensures compatibility with previous auto which allowed conv on closed
terms)
Document Hint Variables
|
|
|
|
It was used in some examples, but never fully documented
|
|
|
|
|
|
|
|
|
|
The test isn't quite the one in #7421 because that use of algebraic
universes is wrong.
|
|
We split a Require Import in two to avoid reaching the timeout.
|
|
|
|
|
|
Many still remain.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
As discussed in GH-7556.
|
|
It failed to compile before because the type arguments were declared implicit after introducing the notation
|
|
|
|
|
|
|
|
|
|
Including a fix to the example given in #7407.
|
|
|
|
|
|
And marginal improvements in the last section of the Gallina chapter.
|
|
|
|
|
|
Not only are most of "forall"s in the manual in Coq notation, but the
math notation leads to have a specially long space after the comma.
|
|
|
|
|
|
|
|
|
|
|
|
and indentation.
|
|
|
|
|
|
|
|
|
|
|
