diff options
| author | Pierre-Marie Pédrot | 2018-12-05 17:41:33 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-12-05 17:41:33 +0100 |
| commit | ce4910fe9299bbd54a313980eedaf8d57daade1c (patch) | |
| tree | 4b758b6af09181d86f5b614141d4460f34d923e8 /stm | |
| parent | 23f2222bb2c97110b6e55835fd19528177e41ff3 (diff) | |
| parent | 3429abee7c572676fa1155bf1620386bdf10d798 (diff) | |
Merge PR #8705: [vernac] [hooks] Refactor towards optional hooks.
Diffstat (limited to 'stm')
| -rw-r--r-- | stm/stm.ml | 7 |
1 files changed, 3 insertions, 4 deletions
diff --git a/stm/stm.ml b/stm/stm.ml index 94405924b7..3444229735 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -1543,7 +1543,7 @@ end = struct (* {{{ *) let pobject, _ = Proof_global.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 [] (mk_hook (fun _ _ -> ()))) in + Lemmas.(standard_proof_terminator []) in let st = Vernacstate.freeze_interp_state `No in stm_vernac_interp stop @@ -1682,9 +1682,8 @@ end = struct (* {{{ *) `OK_ADMITTED else begin (* The original terminator, a hook, has not been saved in the .vio*) - Proof_global.set_terminator - (Lemmas.standard_proof_terminator [] - (Lemmas.mk_hook (fun _ _ -> ()))); + Proof_global.set_terminator (Lemmas.standard_proof_terminator []); + let opaque = Proof_global.Opaque in let proof = Proof_global.close_proof ~opaque ~keep_body_ucst_separate:true (fun x -> x) in |