diff options
| author | Emilio Jesus Gallego Arias | 2018-04-08 03:51:00 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-03-27 23:22:50 +0100 |
| commit | 54a2a3a07e14c597b264566e01d2ecc69c4bd90c (patch) | |
| tree | 52defd39c09a3f981859e053e80946b5495c2039 /plugins/ltac | |
| parent | 3b95c063fae710bc7a943e0dd02617bac09c21bc (diff) | |
[tactic] Adapt tactic layer to removal of imperative proof state.
State in `Proof_global` was mostly used for debugging, so not a big
change.
Diffstat (limited to 'plugins/ltac')
0 files changed, 0 insertions, 0 deletions