[vernac] Unify declaration hooks.

Supersedes #8718.

11 files changed, 139 insertions, 142 deletions

diff --git a/vernac/class.ml b/vernac/class.ml
index 823177d4d1..a6b3242cae 100644
--- a/vernac/class.ml
+++ b/vernac/class.ml
@@ -302,7 +302,7 @@ let try_add_new_identity_coercion id ~local poly ~source ~target =
 let try_add_new_coercion_with_source ref ~local poly ~source =
   try_add_new_coercion_core ref ~local poly (Some source) None false
 
-let add_coercion_hook poly local ref =
+let add_coercion_hook poly _uctx _trans local ref =
   let local = match local with
   | Discharge
   | Local -> true
@@ -314,7 +314,7 @@ let add_coercion_hook poly local ref =
 
 let add_coercion_hook poly = Lemmas.mk_hook (add_coercion_hook poly)
 
-let add_subclass_hook poly local ref =
+let add_subclass_hook poly _uctx _trans local ref =
   let stre = match local with
   | Local -> true
   | Global -> false
diff --git a/vernac/classes.ml b/vernac/classes.ml
index 39c086eff5..263ebf5f5a 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -161,10 +161,10 @@ let declare_instance_open env sigma ?hook ~tac ~program_mode ~global ~poly k id
         in obls, Some constr, typ
       | None -> [||], None, termtype
     in
-    let univ_hook = Obligations.mk_univ_hook hook in
+    let hook = Lemmas.mk_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) ~univ_hook obls)
+              ~univdecl:decl typ ctx ~kind:(Global,poly,Instance) ~hook obls)
   else
     Flags.silently (fun () ->
         (* spiwack: it is hard to reorder the actions to do
@@ -175,7 +175,7 @@ let declare_instance_open env sigma ?hook ~tac ~program_mode ~global ~poly k id
         let sigma = Evd.reset_future_goals sigma in
         Lemmas.start_proof id ~pl:decl kind sigma (EConstr.of_constr termtype)
           ~hook:(Lemmas.mk_hook
-             (fun _ -> instance_hook k pri global imps ?hook));
+             (fun _ _ _ -> instance_hook k pri global imps ?hook));
         (* spiwack: I don't know what to do with the status here. *)
         if not (Option.is_empty term) then
           let init_refine =
diff --git a/vernac/comDefinition.ml b/vernac/comDefinition.ml
index 5eb19eef54..28773a3965 100644
--- a/vernac/comDefinition.ml
+++ b/vernac/comDefinition.ml
@@ -94,22 +94,24 @@ let do_definition ~program_mode ?hook ident k univdecl bl red_option c ctypopt =
   let (ce, evd, univdecl, imps as def) =
     interp_definition ~program_mode univdecl bl (pi2 k) red_option c ctypopt
   in
-    if program_mode then
-      let env = Global.env () in
-      let (c,ctx), sideff = Future.force ce.const_entry_body in
-      assert(Safe_typing.empty_private_constants = sideff);
-      assert(Univ.ContextSet.is_empty ctx);
-      let typ = match ce.const_entry_type with
-        | Some t -> t
-        | None -> EConstr.to_constr ~abort_on_undefined_evars:false evd (Retyping.get_type_of env evd (EConstr.of_constr c))
-      in
-      Obligations.check_evars env evd;
-      let obls, _, c, cty =
-        Obligations.eterm_obligations env ident evd 0 c typ
-      in
-      let ctx = Evd.evar_universe_context evd in
-      let univ_hook = Obligations.mk_univ_hook (fun _ _ l r -> Lemmas.call_hook ?hook l r) in
-      ignore(Obligations.add_definition
-          ident ~term:c cty ctx ~univdecl ~implicits:imps ~kind:k ~univ_hook obls)
-    else let ce = check_definition ~program_mode def in
-      ignore(DeclareDef.declare_definition ident k ce (Evd.universe_binders evd) imps ?hook)
+  if program_mode then
+    let env = Global.env () in
+    let (c,ctx), sideff = Future.force ce.const_entry_body in
+    assert(Safe_typing.empty_private_constants = sideff);
+    assert(Univ.ContextSet.is_empty ctx);
+    let typ = match ce.const_entry_type with
+      | Some t -> t
+      | None -> EConstr.to_constr ~abort_on_undefined_evars:false evd (Retyping.get_type_of env evd (EConstr.of_constr c))
+    in
+    Obligations.check_evars env evd;
+    let obls, _, c, cty =
+      Obligations.eterm_obligations env ident evd 0 c typ
+    in
+    let ctx = Evd.evar_universe_context evd in
+    ignore(Obligations.add_definition
+             ident ~term:c cty ctx ~univdecl ~implicits:imps ~kind:k ?hook obls)
+  else
+    let ce = check_definition ~program_mode def in
+    let uctx = Evd.evar_universe_context evd in
+    let hook_data = Option.map (fun hook -> hook, uctx, []) hook in
+    ignore(DeclareDef.declare_definition ident k ?hook_data ce (Evd.universe_binders evd) imps )
diff --git a/vernac/comProgramFixpoint.ml b/vernac/comProgramFixpoint.ml
index a30313d37c..cc9c83bd17 100644
--- a/vernac/comProgramFixpoint.ml
+++ b/vernac/comProgramFixpoint.ml
@@ -227,7 +227,7 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation =
       in hook, recname, typ
   in
   (* XXX: Capturing sigma here... bad bad *)
-  let univ_hook = Obligations.mk_univ_hook (hook sigma) in
+  let hook = Lemmas.mk_hook (hook sigma) in
   (* XXX: Grounding non-ground terms here... bad bad *)
   let fullcoqc = EConstr.to_constr ~abort_on_undefined_evars:false sigma def in
   let fullctyp = EConstr.to_constr sigma typ in
@@ -237,7 +237,7 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation =
   in
   let ctx = Evd.evar_universe_context sigma in
     ignore(Obligations.add_definition recname ~term:evars_def ~univdecl:decl
-             evars_typ ctx evars ~univ_hook)
+             evars_typ ctx evars ~hook)
 
 let out_def = function
   | Some def -> def
diff --git a/vernac/declareDef.ml b/vernac/declareDef.ml
index 361ed1a737..7dcd098183 100644
--- a/vernac/declareDef.ml
+++ b/vernac/declareDef.ml
@@ -33,7 +33,7 @@ let get_locality id ~kind = function
 | Local -> true
 | Global -> false
 
-let declare_definition ident (local, p, k) ?hook ce pl imps =
+let declare_definition ident (local, p, k) ?hook_data ce pl imps =
   let fix_exn = Future.fix_exn_of ce.const_entry_body in
   let gr = match local with
   | Discharge when Lib.sections_are_opened () ->
@@ -49,11 +49,17 @@ let declare_definition ident (local, p, k) ?hook ce pl imps =
   in
   let () = maybe_declare_manual_implicits false gr imps in
   let () = definition_message ident in
-  Lemmas.call_hook ~fix_exn ?hook local gr; gr
+  begin
+    match hook_data with
+    | None -> ()
+    | Some (hook, uctx, extra_defs) ->
+      Lemmas.call_hook ~fix_exn ~hook uctx extra_defs local gr
+  end;
+  gr
 
-let declare_fix ?(opaque = false) (_,poly,_ as kind) pl univs f ((def,_),eff) t imps =
+let declare_fix ?(opaque = false) ?hook_data (_,poly,_ as kind) pl univs f ((def,_),eff) t imps =
   let ce = definition_entry ~opaque ~types:t ~univs ~eff def in
-  declare_definition f kind ce pl imps
+  declare_definition f kind ?hook_data ce pl imps
 
 let check_definition_evars ~allow_evars sigma =
   let env = Global.env () in
diff --git a/vernac/declareDef.mli b/vernac/declareDef.mli
index e455b59ab2..3f95ec7107 100644
--- a/vernac/declareDef.mli
+++ b/vernac/declareDef.mli
@@ -13,16 +13,26 @@ open Decl_kinds
 
 val get_locality : Id.t -> kind:string -> Decl_kinds.locality -> bool
 
-val declare_definition : Id.t -> definition_kind ->
-  ?hook:Lemmas.declaration_hook ->
-  Safe_typing.private_constants Entries.definition_entry -> UnivNames.universe_binders -> Impargs.manual_implicits ->
-  GlobRef.t
+val declare_definition
+  :  Id.t
+  -> definition_kind
+  -> ?hook_data:(Lemmas.declaration_hook * UState.t * (Id.t * Constr.t) list)
+  -> Safe_typing.private_constants Entries.definition_entry
+  -> UnivNames.universe_binders
+  -> Impargs.manual_implicits
+  -> GlobRef.t
 
-val declare_fix : ?opaque:bool -> definition_kind ->
-  UnivNames.universe_binders -> Entries.universes_entry ->
-  Id.t -> Safe_typing.private_constants Entries.proof_output ->
-  Constr.types -> Impargs.manual_implicits ->
-  GlobRef.t
+val declare_fix
+  :  ?opaque:bool
+  -> ?hook_data:(Lemmas.declaration_hook * UState.t * (Id.t * Constr.t) list)
+  -> definition_kind
+  -> UnivNames.universe_binders
+  -> Entries.universes_entry
+  -> Id.t
+  -> Safe_typing.private_constants Entries.proof_output
+  -> Constr.types
+  -> Impargs.manual_implicits
+  -> GlobRef.t
 
 val prepare_definition : allow_evars:bool ->
   ?opaque:bool -> ?inline:bool -> poly:bool ->
diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index 83dd1aa8e4..77f125e878 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -34,10 +34,13 @@ open Impargs
 module RelDecl = Context.Rel.Declaration
 module NamedDecl = Context.Named.Declaration
 
-type declaration_hook = Decl_kinds.locality -> GlobRef.t -> unit
+type hook_type = UState.t -> (Id.t * Constr.t) list -> Decl_kinds.locality -> GlobRef.t -> unit
+type declaration_hook = hook_type
+
 let mk_hook hook = hook
-let call_hook ?hook ?fix_exn l c =
-  try Option.iter (fun hook -> hook l c) hook
+
+let call_hook ?hook ?fix_exn uctx trans l c =
+  try Option.iter (fun hook -> hook uctx trans l c) hook
   with e when CErrors.noncritical e ->
     let e = CErrors.push e in
     let e = Option.cata (fun fix -> fix e) e fix_exn in
@@ -174,7 +177,7 @@ let look_for_possibly_mutual_statements sigma = function
 
 (* Saving a goal *)
 
-let save ?export_seff id const uctx do_guard (locality,poly,kind) hook =
+let save ?export_seff id const uctx do_guard (locality,poly,kind) hook universes =
   let fix_exn = Future.fix_exn_of const.Entries.const_entry_body in
   try
     let const = adjust_guardness_conditions const do_guard in
@@ -203,7 +206,7 @@ let save ?export_seff id const uctx do_guard (locality,poly,kind) hook =
           gr
     in
     definition_message id;
-    call_hook ?hook locality r
+    call_hook ?hook universes [] locality r
   with e when CErrors.noncritical e ->
     let e = CErrors.push e in
     iraise (fix_exn e)
@@ -289,7 +292,7 @@ let warn_let_as_axiom =
                    (fun id -> strbrk "Let definition" ++ spc () ++ Id.print id ++
                                 spc () ++ strbrk "declared as an axiom.")
 
-let admit ?hook (id,k,e) pl () =
+let admit ?hook ctx (id,k,e) pl () =
   let kn = declare_constant id (ParameterEntry e, IsAssumption Conjectural) in
   let () = match k with
   | Global, _, _ -> ()
@@ -297,16 +300,15 @@ let admit ?hook (id,k,e) pl () =
   in
   let () = assumption_message id in
   Declare.declare_univ_binders (ConstRef kn) pl;
-  call_hook ?hook Global (ConstRef kn)
+  call_hook ?hook ctx [] Global (ConstRef kn)
 
 (* Starting a goal *)
 
-let universe_proof_terminator ?univ_hook compute_guard =
+let standard_proof_terminator ?(hook : declaration_hook option) compute_guard =
   let open Proof_global in
   make_terminator begin function
   | Admitted (id,k,pe,ctx) ->
-    let hook = Option.map (fun univ_hook -> univ_hook (Some ctx)) univ_hook in
-    admit ?hook (id,k,pe) (UState.universe_binders ctx) ();
+    let () = admit ?hook ctx (id,k,pe) (UState.universe_binders ctx) () in
     Feedback.feedback Feedback.AddedAxiom
   | Proved (opaque,idopt, { id; entries=[const]; persistence; universes } ) ->
     let is_opaque, export_seff = match opaque with
@@ -317,16 +319,12 @@ let universe_proof_terminator ?univ_hook compute_guard =
     let id = match idopt with
       | None -> id
       | Some { CAst.v = save_id } -> check_anonymity id save_id; save_id in
-    let hook = Option.map (fun univ_hook -> univ_hook (Some universes)) univ_hook in
-    save ~export_seff id const universes compute_guard persistence hook
+    let () = save ~export_seff id const universes compute_guard persistence hook universes in
+    ()
   | Proved (opaque,idopt, _ ) ->
     CErrors.anomaly Pp.(str "[universe_proof_terminator] close_proof returned more than one proof term")
   end
 
-let standard_proof_terminator ?hook compute_guard =
-  let univ_hook = Option.map (fun hook _ -> hook) hook in
-  universe_proof_terminator ?univ_hook compute_guard
-
 let initialize_named_context_for_proof () =
   let sign = Global.named_context () in
   List.fold_right
@@ -335,7 +333,7 @@ let initialize_named_context_for_proof () =
       let d = if variable_opacity id then NamedDecl.LocalAssum (id, NamedDecl.get_type d) else d in
       Environ.push_named_context_val d signv) sign Environ.empty_named_context_val
 
-let start_proof id ?pl kind sigma ?terminator ?sign ?(compute_guard=[]) ?hook c =
+let start_proof id ?pl kind sigma ?terminator ?sign ?(compute_guard=[]) ?(hook : declaration_hook option) c =
   let terminator = match terminator with
   | None -> standard_proof_terminator ?hook compute_guard
   | Some terminator -> terminator ?hook compute_guard
@@ -348,20 +346,6 @@ let start_proof id ?pl kind sigma ?terminator ?sign ?(compute_guard=[]) ?hook c
   let goals = [ Global.env_of_context sign , c ] in
   Proof_global.start_proof sigma id ?pl kind goals terminator
 
-let start_proof_univs id ?pl kind sigma ?terminator ?sign ?(compute_guard=[]) ?univ_hook c =
-  let terminator = match terminator with
-  | None ->
-    universe_proof_terminator ?univ_hook compute_guard
-  | Some terminator -> terminator ?univ_hook compute_guard
-  in
-  let sign =
-    match sign with
-    | Some sign -> sign
-    | None -> initialize_named_context_for_proof ()
-  in
-  let goals = [ Global.env_of_context sign , c ] in
-  Proof_global.start_proof sigma id ?pl kind goals terminator
-
 let rec_tac_initializer finite guard thms snl =
   if finite then
     match List.map (fun (id,(t,_)) -> (id,t)) thms with
@@ -394,11 +378,7 @@ let start_proof_with_initialization ?hook kind sigma decl recguard thms snl =
   match thms with
   | [] -> anomaly (Pp.str "No proof to start.")
   | (id,(t,(_,imps)))::other_thms ->
-      let hook ctx strength ref =
-        let ctx = match ctx with
-        | None -> UState.empty
-        | Some ctx -> ctx
-        in
+      let hook ctx _ strength ref =
         let other_thms_data =
           if List.is_empty other_thms then [] else
             (* there are several theorems defined mutually *)
@@ -410,8 +390,8 @@ let start_proof_with_initialization ?hook kind sigma decl recguard thms snl =
         let thms_data = (strength,ref,imps)::other_thms_data in
         List.iter (fun (strength,ref,imps) ->
 	  maybe_declare_manual_implicits false ref imps;
-          call_hook ?hook strength ref) thms_data in
-      start_proof_univs id ~pl:decl kind sigma t ~univ_hook:(fun ctx -> mk_hook (hook ctx)) ~compute_guard:guard;
+          call_hook ?hook ctx [] strength ref) thms_data in
+      start_proof id ~pl:decl kind sigma t ~hook ~compute_guard:guard;
       ignore (Proof_global.with_current_proof (fun _ p ->
           match init_tac with
           | None -> p,(true,[])
diff --git a/vernac/lemmas.mli b/vernac/lemmas.mli
index a9a10a6e38..72c666e903 100644
--- a/vernac/lemmas.mli
+++ b/vernac/lemmas.mli
@@ -13,10 +13,29 @@ open Decl_kinds
 
 type declaration_hook
 
-val mk_hook : (Decl_kinds.locality -> GlobRef.t -> unit) -> declaration_hook
-val call_hook :
-  ?hook:declaration_hook -> ?fix_exn:Future.fix_exn ->
-  Decl_kinds.locality -> GlobRef.t -> unit
+(* Hooks allow users of the API to perform arbitrary actions at
+ * proof/definition saving time. For example, to register a constant
+ * as a Coercion, perform some cleanup, update the search database,
+ * etc...
+ *
+ * Here, we use an extended hook type suitable for obligations /
+ * equations.
+ *)
+(** [hook_type] passes to the client:
+    - [ustate]: universe constraints obtained when the term was closed
+    - [(n1,t1),...(nm,tm)]: association list between obligation
+        name and the corresponding defined term (might be a constant,
+        but also an arbitrary term in the Expand case of obligations)
+    - [locality]: Locality of the original declaration
+    - [ref]: identifier of the origianl declaration
+ *)
+type hook_type = UState.t -> (Id.t * Constr.t) list -> Decl_kinds.locality -> GlobRef.t -> unit
+
+val mk_hook : hook_type -> declaration_hook
+val call_hook
+  :  ?hook:declaration_hook
+  -> ?fix_exn:Future.fix_exn
+  -> hook_type
 
 val start_proof : Id.t -> ?pl:UState.universe_decl -> goal_kind -> Evd.evar_map ->
   ?terminator:(?hook:declaration_hook -> Proof_global.lemma_possible_guards -> Proof_global.proof_terminator) ->
@@ -24,12 +43,6 @@ val start_proof : Id.t -> ?pl:UState.universe_decl -> goal_kind -> Evd.evar_map
   ?compute_guard:Proof_global.lemma_possible_guards ->
   ?hook:declaration_hook ->  EConstr.types -> unit
 
-val start_proof_univs : Id.t -> ?pl:UState.universe_decl -> goal_kind -> Evd.evar_map ->
-  ?terminator:(?univ_hook:(UState.t option -> declaration_hook) -> Proof_global.lemma_possible_guards -> Proof_global.proof_terminator) ->
-  ?sign:Environ.named_context_val ->
-  ?compute_guard:Proof_global.lemma_possible_guards ->
-  ?univ_hook:(UState.t option -> declaration_hook) -> EConstr.types -> unit
-
 val start_proof_com :
   program_mode:bool -> ?inference_hook:Pretyping.inference_hook ->
   ?hook:declaration_hook -> goal_kind -> Vernacexpr.proof_expr list ->
@@ -43,11 +56,6 @@ val start_proof_with_initialization :
      (EConstr.types (* type of thm *) * (Name.t list (* names to pre-introduce *) * Impargs.manual_explicitation list))) list ->
   int list option -> unit
 
-val universe_proof_terminator :
-  ?univ_hook:(UState.t option -> declaration_hook) ->
-  Proof_global.lemma_possible_guards ->
-  Proof_global.proof_terminator
-
 val standard_proof_terminator :
   ?hook:declaration_hook -> Proof_global.lemma_possible_guards ->
   Proof_global.proof_terminator
diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index ba78c73131..38cdfc2d7a 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -20,15 +20,6 @@ open Pp
 open CErrors
 open Util
 
-type univ_declaration_hook = UState.t -> (Id.t * constr) list -> Decl_kinds.locality -> GlobRef.t -> unit
-let mk_univ_hook f = f
-let call_univ_hook ?univ_hook ?fix_exn uctx trans l c =
-  try Option.iter (fun hook -> hook uctx trans l c) univ_hook
-  with e when CErrors.noncritical e ->
-    let e = CErrors.push e in
-    let e = Option.cata (fun fix -> fix e) e fix_exn in
-    iraise e
-
 module NamedDecl = Context.Named.Declaration
 
 let get_fix_exn, stm_get_fix_exn = Hook.make ()
@@ -321,7 +312,7 @@ type program_info_aux = {
   prg_notations : notations ;
   prg_kind : definition_kind;
   prg_reduce : constr -> constr;
-  prg_hook : univ_declaration_hook option;
+  prg_hook : Lemmas.declaration_hook option;
   prg_opaque : bool;
   prg_sign: named_context_val;
 }
@@ -482,9 +473,9 @@ let declare_definition prg =
   let ce = definition_entry ~fix_exn ~opaque ~types:typ ~univs body in
   let () = progmap_remove prg in
   let ubinders = UState.universe_binders uctx in
-  let hook = Lemmas.mk_hook (fun l r -> call_univ_hook ?univ_hook:prg.prg_hook ~fix_exn uctx obls l r; ()) in
+  let hook_data = Option.map (fun hook -> hook, uctx, obls) prg.prg_hook in
   DeclareDef.declare_definition prg.prg_name
-    prg.prg_kind ce ubinders prg.prg_implicits ~hook
+    prg.prg_kind ce ubinders prg.prg_implicits ?hook_data
 
 let rec lam_index n t acc =
   match Constr.kind t with
@@ -559,14 +550,16 @@ let declare_mutual_definition l =
   (* Declare the recursive definitions *)
   let univs = UState.univ_entry ~poly first.prg_ctx in
   let fix_exn = Hook.get get_fix_exn () in
-  let kns = List.map4 (DeclareDef.declare_fix ~opaque (local, poly, kind) UnivNames.empty_binders univs)
-    fixnames fixdecls fixtypes fiximps in
-    (* Declare notations *)
-    List.iter (Metasyntax.add_notation_interpretation (Global.env())) first.prg_notations;
-    Declare.recursive_message (fixkind != IsCoFixpoint) indexes fixnames;
-    let gr = List.hd kns in
-    call_univ_hook ?univ_hook:first.prg_hook ~fix_exn first.prg_ctx obls local gr;
-    List.iter progmap_remove l; gr
+  let kns = List.map4
+      (DeclareDef.declare_fix ~opaque (local, poly, kind) UnivNames.empty_binders univs)
+      fixnames fixdecls fixtypes fiximps
+  in
+  (* Declare notations *)
+  List.iter (Metasyntax.add_notation_interpretation (Global.env())) first.prg_notations;
+  Declare.recursive_message (fixkind != IsCoFixpoint) indexes fixnames;
+  let gr = List.hd kns in
+  Lemmas.call_hook ?hook:first.prg_hook ~fix_exn first.prg_ctx obls local gr;
+  List.iter progmap_remove l; gr
 
 let decompose_lam_prod c ty =
   let open Context.Rel.Declaration in
@@ -663,7 +656,7 @@ let declare_obligation prg obl body ty uctx =
       in
       true, { obl with obl_body = body }
 
-let init_prog_info ?(opaque = false) ?univ_hook sign n udecl b t ctx deps fixkind
+let init_prog_info ?(opaque = false) ?hook sign n udecl b t ctx deps fixkind
                    notations obls impls kind reduce =
   let obls', b =
     match b with
@@ -689,7 +682,7 @@ let init_prog_info ?(opaque = false) ?univ_hook sign n udecl b t ctx deps fixkin
       prg_obligations = (obls', Array.length obls');
       prg_deps = deps; prg_fixkind = fixkind ; prg_notations = notations ;
       prg_implicits = impls; prg_kind = kind; prg_reduce = reduce; 
-      prg_hook = univ_hook; prg_opaque = opaque;
+      prg_hook = hook; prg_opaque = opaque;
       prg_sign = sign }
 
 let map_cardinal m =
@@ -844,9 +837,9 @@ let solve_by_tac ?loc name evi t poly ctx =
     warn_solve_errored ?loc err;
     None
 
-let obligation_terminator ?univ_hook name num guard auto pf =
+let obligation_terminator ?hook name num guard auto pf =
   let open Proof_global in
-  let term = Lemmas.universe_proof_terminator ?univ_hook guard in
+  let term = Lemmas.standard_proof_terminator ?hook guard in
   match pf with
   | Admitted _ -> apply_terminator term pf
   | Proved (opq, id, { entries=[entry]; universes=uctx } ) -> begin
@@ -912,7 +905,7 @@ let obligation_terminator ?univ_hook name num guard auto pf =
   | Proved (_, _, _ ) ->
     CErrors.anomaly Pp.(str "[obligation_terminator] close_proof returned more than one proof term")
 
-let obligation_hook prg obl num auto ctx' _ gr =
+let obligation_hook prg obl num auto ctx' _ _ gr =
   let obls, rem = prg.prg_obligations in
   let cst = match gr with GlobRef.ConstRef cst -> cst | _ -> assert false in
   let transparent = evaluable_constant cst (Global.env ()) in
@@ -922,7 +915,6 @@ let obligation_hook prg obl num auto ctx' _ gr =
        if not transparent then err_not_transp ()
     | _ -> ()
   in
-  let ctx' = match ctx' with None -> prg.prg_ctx | Some ctx' -> ctx' in
   let inst, ctx' =
     if not (pi2 prg.prg_kind) (* Not polymorphic *) then
       (* The universe context was declared globally, we continue
@@ -969,11 +961,11 @@ let rec solve_obligation prg num tac =
   let evd = Evd.from_ctx prg.prg_ctx in
   let evd = Evd.update_sigma_env evd (Global.env ()) in
   let auto n tac oblset = auto_solve_obligations n ~oblset tac in
-  let terminator ?univ_hook guard =
+  let terminator ?hook guard =
     Proof_global.make_terminator
-      (obligation_terminator ?univ_hook prg.prg_name num guard auto) in
-  let univ_hook ctx = Lemmas.mk_hook (obligation_hook prg obl num auto ctx) in
-  let () = Lemmas.start_proof_univs ~sign:prg.prg_sign obl.obl_name kind evd (EConstr.of_constr obl.obl_type) ~terminator ~univ_hook in
+      (obligation_terminator ?hook prg.prg_name num guard auto) in
+  let hook = Lemmas.mk_hook (obligation_hook prg obl num auto) in
+  let () = Lemmas.start_proof ~sign:prg.prg_sign obl.obl_name kind evd (EConstr.of_constr obl.obl_type) ~terminator ~hook in
   let _ = Pfedit.by !default_tactic in
   Option.iter (fun tac -> Proof_global.set_endline_tactic tac) tac
 
@@ -1110,10 +1102,10 @@ let show_term n =
 
 let add_definition n ?term t ctx ?(univdecl=UState.default_univ_decl)
                    ?(implicits=[]) ?(kind=Global,false,Definition) ?tactic
-    ?(reduce=reduce) ?univ_hook ?(opaque = false) obls =
+    ?(reduce=reduce) ?hook ?(opaque = false) obls =
   let sign = Lemmas.initialize_named_context_for_proof () in
   let info = Id.print n ++ str " has type-checked" in
-  let prg = init_prog_info sign ~opaque n univdecl term t ctx [] None [] obls implicits kind reduce ?univ_hook in
+  let prg = init_prog_info sign ~opaque n univdecl term t ctx [] None [] obls implicits kind reduce ?hook in
   let obls,_ = prg.prg_obligations in
   if Int.equal (Array.length obls) 0 then (
     Flags.if_verbose Feedback.msg_info (info ++ str ".");
@@ -1130,13 +1122,13 @@ let add_definition n ?term t ctx ?(univdecl=UState.default_univ_decl)
 
 let add_mutual_definitions l ctx ?(univdecl=UState.default_univ_decl) ?tactic
                            ?(kind=Global,false,Definition) ?(reduce=reduce)
-    ?univ_hook ?(opaque = false) notations fixkind =
+    ?hook ?(opaque = false) notations fixkind =
   let sign = Lemmas.initialize_named_context_for_proof () in
   let deps = List.map (fun (n, b, t, imps, obls) -> n) l in
     List.iter
     (fun  (n, b, t, imps, obls) ->
      let prg = init_prog_info sign ~opaque n univdecl (Some b) t ctx deps (Some fixkind)
-       notations obls imps kind reduce ?univ_hook
+       notations obls imps kind reduce ?hook
      in progmap_add n (CEphemeron.create prg)) l;
     let _defined =
       List.fold_left (fun finished x ->
diff --git a/vernac/obligations.mli b/vernac/obligations.mli
index 4eef668f56..c5720363b4 100644
--- a/vernac/obligations.mli
+++ b/vernac/obligations.mli
@@ -13,12 +13,6 @@ open Constr
 open Evd
 open Names
 
-type univ_declaration_hook
-val mk_univ_hook : (UState.t -> (Id.t * constr) list -> Decl_kinds.locality -> GlobRef.t -> unit) ->
-  univ_declaration_hook
-val call_univ_hook : ?univ_hook:univ_declaration_hook -> ?fix_exn:Future.fix_exn ->
-  UState.t -> (Id.t * constr) list -> Decl_kinds.locality -> GlobRef.t -> unit
-
 (* This is a hack to make it possible for Obligations to craft a Qed
  * behind the scenes.  The fix_exn the Stm attaches to the Future proof
  * is not available here, so we provide a side channel to get it *)
@@ -58,14 +52,19 @@ type progress = (* Resolution status of a program *)
 
 val default_tactic : unit Proofview.tactic ref
 
-val add_definition : Names.Id.t -> ?term:constr -> types ->
-  UState.t ->
-  ?univdecl:UState.universe_decl -> (* Universe binders and constraints *)
-  ?implicits:(Constrexpr.explicitation * (bool * bool * bool)) list ->
-  ?kind:Decl_kinds.definition_kind ->
-  ?tactic:unit Proofview.tactic ->
-  ?reduce:(constr -> constr) ->
-  ?univ_hook:univ_declaration_hook -> ?opaque:bool -> obligation_info -> progress
+val add_definition
+  :  Names.Id.t
+  -> ?term:constr -> types
+  -> UState.t
+  -> ?univdecl:UState.universe_decl (* Universe binders and constraints *)
+  -> ?implicits:(Constrexpr.explicitation * (bool * bool * bool)) list
+  -> ?kind:Decl_kinds.definition_kind
+  -> ?tactic:unit Proofview.tactic
+  -> ?reduce:(constr -> constr)
+  -> ?hook:Lemmas.declaration_hook
+  -> ?opaque:bool
+  -> obligation_info
+  -> progress
 
 type notations =
     (lstring * Constrexpr.constr_expr * Notation_term.scope_name option) list
@@ -82,7 +81,7 @@ val add_mutual_definitions :
   ?tactic:unit Proofview.tactic ->
   ?kind:Decl_kinds.definition_kind ->
   ?reduce:(constr -> constr) ->
-  ?univ_hook:univ_declaration_hook -> ?opaque:bool ->
+  ?hook:Lemmas.declaration_hook -> ?opaque:bool ->
   notations ->
   fixpoint_kind -> unit
 
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index d511bcd4fd..11b64a5247 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -542,7 +542,7 @@ let vernac_definition_hook p = function
 | Coercion ->
   Some (Class.add_coercion_hook p)
 | CanonicalStructure ->
-  Some (Lemmas.mk_hook (fun _ -> Recordops.declare_canonical_structure))
+  Some (Lemmas.mk_hook (fun _ _ _ -> Recordops.declare_canonical_structure))
 | SubClass ->
   Some (Class.add_subclass_hook p)
 | _ -> None