diff options
| author | Emilio Jesus Gallego Arias | 2018-04-08 02:23:57 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-03-27 23:22:46 +0100 |
| commit | c643db27da50d947f979e23ef804422d5774d11e (patch) | |
| tree | 659e6265b79df69f27ba5a101ca4d85e475dc3a5 /plugins/syntax/g_string.mlg | |
| parent | a796822e5f57f74ff36e538fd2169f70a8c6c145 (diff) | |
[proof_global] Removal of imperative state.
We change the API; after some thinking the tradeoff is clear in favor
of the more radical functional option from the start.
We also guarante the existence of a proof is by typing now,
so exceptions `NoCurrentProof` and `NoSuchGoal` are gone.
TODO: Review what's going on with focusing now.
Diffstat (limited to 'plugins/syntax/g_string.mlg')
0 files changed, 0 insertions, 0 deletions