| 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.
|
|
|
|
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)
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
needed
|
|
shown in the previous example
|
|
|
|
We have expanded the example above.
For consistency reasons, it would make sense to do the same also for this example.
However, due to the size of the terms, it is hard to typeset it nicely.
I propose to remove it.
|
|
|
