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/classes.ml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'vernac/classes.ml')

diff --git a/vernac/classes.ml b/vernac/classes.ml
index 37ee33b19f..09e2b8df45 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -149,7 +149,7 @@ let do_abstract_instance env sigma ?hook ~global ~poly k u ctx ctx' pri decl imp
 let declare_instance_open env sigma ?hook ~tac ~program_mode ~global ~poly k id pri imps decl len term termtype =
   let kind = Decl_kinds.Global, poly, Decl_kinds.DefinitionBody Decl_kinds.Instance in
   if program_mode then
-    let hook vis gr _ =
+    let hook _ vis gr =
       let cst = match gr with ConstRef kn -> kn | _ -> assert false in
       Impargs.declare_manual_implicits false gr ~enriching:false [imps];
       let pri = intern_info pri in
@@ -163,7 +163,7 @@ let declare_instance_open env sigma ?hook ~tac ~program_mode ~global ~poly k id
         in obls, Some constr, typ
       | None -> [||], None, termtype
     in
-    let hook = Lemmas.mk_hook hook in
+    let hook = Obligations.mk_univ_hook hook in
     let ctx = Evd.evar_universe_context sigma in
     ignore (Obligations.add_definition id ?term:constr
               ~univdecl:decl typ ctx ~kind:(Global,poly,Instance) ~hook obls)
@@ -425,7 +425,7 @@ let context poly l =
       | Some b ->
         let decl = (Discharge, poly, Definition) in
         let entry = Declare.definition_entry ~univs ~types:t b in
-        let hook = Lemmas.mk_hook (fun _ gr -> gr) in
+        let hook = Lemmas.mk_hook (fun _ _ -> ()) in
         let _ = DeclareDef.declare_definition id decl entry UnivNames.empty_binders [] hook in
         Lib.sections_are_opened () || Lib.is_modtype_strict ()
       in
-- 
cgit v1.2.3