diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-12-01 20:29:13 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-12-04 12:21:38 +0100 |
| commit | 195a652e38bcb6f58c156495492999ea8ee4e64e (patch) | |
| tree | 19788da699483c51d3560feb435fbec880d85911 /vernac/vernacentries.ml | |
| parent | 0048cbe810c82a775558c14cd7fcae644e205c51 (diff) | |
[vernac] Couple of tweaks missing from previous PRs.
In particular we must invalidate the state cache in the case of an
exception.
Diffstat (limited to 'vernac/vernacentries.ml')
| -rw-r--r-- | vernac/vernacentries.ml | 9 |
1 files changed, 7 insertions, 2 deletions
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index f8ec05fdb..63768d9b8 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -2268,5 +2268,10 @@ let interp ?(verbosely=true) ?proof ~st (loc,c) = comments on the PR *) let interp ?verbosely ?proof ~st cmd = Vernacstate.unfreeze_interp_state st; - interp ?verbosely ?proof ~st cmd; - Vernacstate.freeze_interp_state `No + try + interp ?verbosely ?proof ~st cmd; + Vernacstate.freeze_interp_state `No + with exn -> + let exn = CErrors.push exn in + Vernacstate.invalidate_cache (); + iraise exn |