| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
|
|
|
|
|
|
This is useful for restoring bullets after e.g. loading ssreflect.
Hoping Arnaud is ok in documenting it.
|
|
Following a discussion on coq-club on Jan 13, 2016.
|
|
|
|
In particular, documenting bracketing of last pattern on by default.
|
|
enough
In particular, its interface might still change (in interaction with interested
colleagues). So let's not give it too much visibility yet. Instead, I'll turn
it as an opam packages for now.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
The option is still there, but not documented since it is too
dangerous. Hints and type classes instances are not taking cleared
variables into account.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Marking it as experimental.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
global environment (we use throughout the document)
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
