From 3429abee7c572676fa1155bf1620386bdf10d798 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Thu, 11 Oct 2018 00:20:24 +0200
Subject: [vernac] [hooks] Refactor towards optional hooks.

We make `declaration_hook`s optional arguments everywhere, and thus we
avoid some "fake" functions having to be passed.

This identifies positively the code really using hooks [funind,
rewrite, coercions, program, and canonicals] and helps moving toward
some hope of reification.
---
 stm/stm.ml | 7 +++----
 1 file changed, 3 insertions(+), 4 deletions(-)

(limited to 'stm')

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