| Commit message (Collapse) | Author | Age |
| |
|
|
|
|
|
| |
In particular `Proof_global.t` will become a first class object for
the upper parts of the system in a next commit.
|
|
|
|
|
|
|
| |
This is a continuation on #6183 and another step towards a more
functional interpretation of commands.
In particular, this should allow us to remove the locality hack.
|
|
To this purpose we allow plugins to register functions that will
modify the state.
This is not used yet, but will be used soon when we remove the global
handling of the proof state.
|