diff options
| author | Emilio Jesus Gallego Arias | 2019-02-24 01:57:59 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-06-17 12:30:13 +0200 |
| commit | a2ea73d84be2fe95eeda42f5f5ac458f0af9968f (patch) | |
| tree | 0b3c485f6e196bb74dca8c2eda6a6cf2448b2745 /stm | |
| parent | 5d18dfed8e68dd964bca5d64ca6bdd9f8ffbb1df (diff) | |
[proofs] Store hooks in the proof object.
As of now, hooks were stored in the terminators as closures, we place
them instead in the proof object and are thus passed back at proof
closing time.
This helps towards the reification and unification of terminators.
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 |