diff options
Diffstat (limited to 'stm')
| -rw-r--r-- | stm/stm.ml | 11 |
1 files changed, 6 insertions, 5 deletions
diff --git a/stm/stm.ml b/stm/stm.ml index d77e37c910..a0247e0d8f 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -1532,14 +1532,15 @@ end = struct (* {{{ *) (* Unfortunately close_future_proof and friends are not pure so we need to set the state manually here *) State.unfreeze st; - let pobject, _ = + let pobject, _terminator, _hook = PG_compat.close_future_proof ~opaque ~feedback_id:stop (Future.from_val ~fix_exn p) in + let terminator = (* The one sent by master is an InvalidKey *) Lemmas.(standard_proof_terminator []) in let st = Vernacstate.freeze_interp_state ~marshallable:false in stm_vernac_interp stop - ~proof:(pobject, terminator) st + ~proof:(pobject, terminator, None) st { verbose = false; indentation = 0; strlen = 0; expr = CAst.make ?loc @@ VernacExpr ([], VernacEndProof (Proved (opaque,None))) }) in ignore(Future.join checked_proof); @@ -1676,10 +1677,10 @@ end = struct (* {{{ *) let opaque = Proof_global.Opaque in (* The original terminator, a hook, has not been saved in the .vio*) - let pterm, _invalid_terminator = + let pterm, _invalid_terminator, _hook = PG_compat.close_proof ~opaque ~keep_body_ucst_separate:true (fun x -> x) in - let proof = pterm , Lemmas.standard_proof_terminator [] in + let proof = pterm , Lemmas.standard_proof_terminator [], None in (* We jump at the beginning since the kernel handles side effects by also * looking at the ones that happen to be present in the current env *) @@ -1734,7 +1735,7 @@ end = struct (* {{{ *) | `ERROR -> exit 1 | `ERROR_ADMITTED -> cst, false | `OK_ADMITTED -> cst, false - | `OK (po,_) -> + | `OK (po,_,_) -> let con = Nametab.locate_constant (Libnames.qualid_of_ident po.Proof_global.id) in |