diff options
| author | Emilio Jesus Gallego Arias | 2018-04-08 09:35:26 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-03-27 23:22:50 +0100 |
| commit | 7efaf86882488034e6545505e1eda7d6e1a6ce14 (patch) | |
| tree | 7a0aafae5d81a510877489500ffa434763315a51 /toplevel/vernac.ml | |
| parent | 54a2a3a07e14c597b264566e01d2ecc69c4bd90c (diff) | |
[vernac] Adapt to removal of imperative proof state.
Diffstat (limited to 'toplevel/vernac.ml')
| -rw-r--r-- | toplevel/vernac.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index ef1dc6993b..ce584f1109 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -70,7 +70,7 @@ let interp_vernac ~check ~interactive ~state ({CAst.loc;_} as com) = (* Force the command *) let ndoc = if check then Stm.observe ~doc nsid else doc in - let new_proof = Proof_global.give_me_the_proof_opt () in + let new_proof = Vernacstate.Proof_global.give_me_the_proof_opt () in { state with doc = ndoc; sid = nsid; proof = new_proof; } with reraise -> (* XXX: In non-interactive mode edit_at seems to do very weird |