diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-11-19 03:40:45 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-11-19 17:38:19 +0100 |
| commit | dc664b3b0c6f6f5eeba0c1092efc3f4537cdf657 (patch) | |
| tree | 228d0aeba91a663b947625fd58cebe5bf4537f08 /plugins/funind | |
| parent | d7a5f439de0208c4a543a81158107b8ccecb6ced (diff) | |
[plugins] Prepare plugin API for functional handling of state.
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.
Diffstat (limited to 'plugins/funind')
| -rw-r--r-- | plugins/funind/indfun_common.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index e9102e9c8..61d207b95 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -550,11 +550,11 @@ type tcc_lemma_value = | Value of constr | Not_needed -(* We only "purify" on exceptions *) +(* We only "purify" on exceptions. XXX: What is this doing here? *) let funind_purify f x = - let st = Vernacentries.freeze_interp_state `No in + let st = Vernacstate.freeze_interp_state `No in try f x with e -> let e = CErrors.push e in - Vernacentries.unfreeze_interp_state st; + Vernacstate.unfreeze_interp_state st; Exninfo.iraise e |