| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
|
|
into JasonGross-trunk-function_scope
|
|
|
|
|
|
|
|
|
|
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.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
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)
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
