| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
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.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Fix Hint (Transparent | Opaque) index.
|
|
Add some more cmd references.
And use deprecated directives.
|
|
In particular, remove trailing dots.
|
|
|
|
|
|
|
|
|
|
|
|
All the error messages start with a capitalized letter and end with a dot.
|
|
|
