| Age | Commit message (Collapse) | Author |
|---|
|
|
|
The readme is auto-generated by combining introductory text with the docstrings
in coqdomain.py.
|
|
Also get rid of a few unused or redundant constructs: the :ltac: role and the
'tac' directive (unused) and the :gallina: and :notation: roles (redundant).
|
|
|
|
|
|
|
|
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.
|
|
|
|
- Remove all trailing dots.
- There is only one Bullet Behavior option.
- Replaces `@natural` and `@integer` by `@num`.
|
|
|
|
|
|
|
|
|
