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.
---
 plugins/ltac/rewrite.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins/ltac')

diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index fee469032c..06783de614 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -1998,7 +1998,7 @@ let add_morphism_infer atts m n =
       let hook = Lemmas.mk_hook hook in
 	Flags.silently
 	  (fun () ->
-	    Lemmas.start_proof instance_id kind (Evd.from_ctx uctx) (EConstr.of_constr instance) hook;
+            Lemmas.start_proof ~hook instance_id kind (Evd.from_ctx uctx) (EConstr.of_constr instance);
 	    ignore (Pfedit.by (Tacinterp.interp tac))) ()
 
 let add_morphism atts binders m s n =
-- 
cgit v1.2.3