From 873281c256fc33941d93044acc3db8eda0a148ee Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Sun, 24 Feb 2019 20:38:21 +0100
Subject: [proof] Move declaration hooks to DeclareDef.

This way both `Lemmas` and `DeclareObl` can depend on it, removing one
more difficulty on the unification of terminators.
---
 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 2da6584aba..2bab55ef74 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -2006,7 +2006,7 @@ let add_morphism_interactive atts m n : Lemmas.t =
       declare_projection n instance_id (ConstRef cst)
     | _ -> assert false
   in
-  let hook = Lemmas.mk_hook hook in
+  let hook = DeclareDef.Hook.make hook in
   Flags.silently
     (fun () ->
        let lemma = Lemmas.start_lemma ~hook instance_id kind (Evd.from_ctx uctx) (EConstr.of_constr instance) in
-- 
cgit v1.2.3