From c8883873426c92778a1cac02da17e3d123beb394 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Wed, 10 Oct 2018 23:35:47 +0200
Subject: [vernac] Remove unused abstraction from declaration_hook type.

"Declaration" hooks can be polymorphic on their return type, however
this facility doesn't seem used in the codebase.

We thus remove the polymorphism with the hope to be able to reify the
control later on.
---
 vernac/comDefinition.ml | 6 ++----
 1 file changed, 2 insertions(+), 4 deletions(-)

(limited to 'vernac/comDefinition.ml')

diff --git a/vernac/comDefinition.ml b/vernac/comDefinition.ml
index a8d7946429..5d17662d1a 100644
--- a/vernac/comDefinition.ml
+++ b/vernac/comDefinition.ml
@@ -127,10 +127,8 @@ let do_definition ~program_mode ident k univdecl bl red_option c ctypopt hook =
         Obligations.eterm_obligations env ident evd 0 c typ
       in
       let ctx = Evd.evar_universe_context evd in
-      let hook = Lemmas.mk_hook (fun l r _ -> Lemmas.call_hook (fun exn -> exn) hook l r) in
+      let hook = Obligations.mk_univ_hook (fun _ l r -> Lemmas.call_hook (fun x -> x) hook l r) in
       ignore(Obligations.add_definition
           ident ~term:c cty ctx ~univdecl ~implicits:imps ~kind:k ~hook obls)
     else let ce = check_definition def in
-      ignore(DeclareDef.declare_definition ident k ce (Evd.universe_binders evd) imps
-        (Lemmas.mk_hook
-          (fun l r -> Lemmas.call_hook (fun exn -> exn) hook l r;r)))
+      ignore(DeclareDef.declare_definition ident k ce (Evd.universe_binders evd) imps hook)
-- 
cgit v1.2.3