From a2ea73d84be2fe95eeda42f5f5ac458f0af9968f Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Sun, 24 Feb 2019 01:57:59 +0100
Subject: [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.
---
 stm/stm.ml | 11 ++++++-----
 1 file changed, 6 insertions(+), 5 deletions(-)

(limited to 'stm')

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
-- 
cgit v1.2.3