Allow program hooks to see the refined universe_context at the end of a

definition, if they manipulate structures depending on the initial state
of the context.

4 files changed, 13 insertions, 11 deletions

diff --git a/toplevel/classes.ml b/toplevel/classes.ml
index c354c7d32..6de0a9f55 100644
--- a/toplevel/classes.ml
+++ b/toplevel/classes.ml
@@ -288,7 +288,7 @@ let new_instance ?(abstract=false) ?(global=false) poly ctx (instid, bk, cl) pro
 	else if !refine_instance || Option.is_empty term then begin
 	  let kind = Decl_kinds.Global, poly, Decl_kinds.DefinitionBody Decl_kinds.Instance in
 	    if Flags.is_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];
 		  Typeclasses.declare_instance pri (not global) (ConstRef cst)
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 3d338ee0a..0b709a3fc 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -192,6 +192,7 @@ let do_definition ident k pl 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
 	ignore(Obligations.add_definition
           ident ~term:c cty ctx ~implicits:imps ~kind:k ~hook obls)
     else let ce = check_definition def in
@@ -1010,7 +1011,7 @@ let build_wellfounded (recname,n,bl,arityc,body) r measure notation =
   let hook, recname, typ = 
     if List.length binders_rel > 1 then
       let name = add_suffix recname "_func" in
-      let hook l gr = 
+      let hook l gr _ = 
 	let body = it_mkLambda_or_LetIn (mkApp (Universes.constr_of_global gr, [|make|])) binders_rel in
 	let ty = it_mkProd_or_LetIn top_arity binders_rel in
 	let pl, univs = Evd.universe_context !evdref in
@@ -1026,7 +1027,7 @@ let build_wellfounded (recname,n,bl,arityc,body) r measure notation =
 	hook, name, typ
     else 
       let typ = it_mkProd_or_LetIn top_arity binders_rel in
-      let hook l gr = 
+      let hook l gr _ = 
 	if Impargs.is_implicit_args () || not (List.is_empty impls) then
 	  Impargs.declare_manual_implicits false gr [impls]
       in hook, recname, typ
diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml
index 9019f486b..311c61f89 100644
--- a/toplevel/obligations.ml
+++ b/toplevel/obligations.ml
@@ -318,7 +318,7 @@ type program_info_aux = {
   prg_notations : notations ;
   prg_kind : definition_kind;
   prg_reduce : constr -> constr;
-  prg_hook : unit Lemmas.declaration_hook;
+  prg_hook : (Evd.evar_universe_context -> unit) Lemmas.declaration_hook;
   prg_opaque : bool;
 }
 
@@ -517,7 +517,7 @@ let declare_definition prg =
     progmap_remove prg;
     !declare_definition_ref prg.prg_name 
       prg.prg_kind ce prg.prg_implicits
-      (Lemmas.mk_hook (fun l r -> Lemmas.call_hook fix_exn prg.prg_hook l r; r))
+      (Lemmas.mk_hook (fun l r -> Lemmas.call_hook fix_exn prg.prg_hook l r prg.prg_ctx; r))
       
 open Pp
 
@@ -582,6 +582,7 @@ let declare_mutual_definition l =
   in
   (* Declare the recursive definitions *)
   let ctx = Evd.evar_context_universe_context first.prg_ctx in
+  let fix_exn = Stm.get_fix_exn () in
   let kns = List.map4 (!declare_fix_ref ~opaque (local, poly, kind) ctx)
     fixnames fixdecls fixtypes fiximps in
     (* Declare notations *)
@@ -589,8 +590,8 @@ let declare_mutual_definition l =
     Declare.recursive_message (fixkind != IsCoFixpoint) indexes fixnames;
     let gr = List.hd kns in
     let kn = match gr with ConstRef kn -> kn | _ -> assert false in
-      Lemmas.call_hook (fun exn -> exn) first.prg_hook local gr;
-      List.iter progmap_remove l; kn
+    Lemmas.call_hook fix_exn first.prg_hook local gr first.prg_ctx;
+    List.iter progmap_remove l; kn
 
 let shrink_body c = 
   let ctx, b = decompose_lam c in
@@ -987,7 +988,7 @@ let show_term n =
 	    ++ Printer.pr_constr_env (Global.env ()) Evd.empty prg.prg_body)
 
 let add_definition n ?term t ctx ?(implicits=[]) ?(kind=Global,false,Definition) ?tactic
-    ?(reduce=reduce) ?(hook=Lemmas.mk_hook (fun _ _ -> ())) ?(opaque = false) obls =
+    ?(reduce=reduce) ?(hook=Lemmas.mk_hook (fun _ _ _ -> ())) ?(opaque = false) obls =
   let info = str (Id.to_string n) ++ str " has type-checked" in
   let prg = init_prog_info ~opaque n term t ctx [] None [] obls implicits kind reduce hook in
   let obls,_ = prg.prg_obligations in
@@ -1005,7 +1006,7 @@ let add_definition n ?term t ctx ?(implicits=[]) ?(kind=Global,false,Definition)
 	| _ -> res)
 
 let add_mutual_definitions l ctx ?tactic ?(kind=Global,false,Definition) ?(reduce=reduce)
-    ?(hook=Lemmas.mk_hook (fun _ _ -> ())) ?(opaque = false) notations fixkind =
+    ?(hook=Lemmas.mk_hook (fun _ _ _ -> ())) ?(opaque = false) notations fixkind =
   let deps = List.map (fun (n, b, t, imps, obls) -> n) l in
     List.iter
     (fun  (n, b, t, imps, obls) ->
diff --git a/toplevel/obligations.mli b/toplevel/obligations.mli
index 61a8ee520..2e3aa6005 100644
--- a/toplevel/obligations.mli
+++ b/toplevel/obligations.mli
@@ -68,7 +68,7 @@ val add_definition : Names.Id.t -> ?term:Term.constr -> Term.types ->
   ?kind:Decl_kinds.definition_kind ->
   ?tactic:unit Proofview.tactic ->
   ?reduce:(Term.constr -> Term.constr) ->
-  ?hook:unit Lemmas.declaration_hook -> ?opaque:bool -> obligation_info -> progress
+  ?hook:(Evd.evar_universe_context -> unit) Lemmas.declaration_hook -> ?opaque:bool -> obligation_info -> progress
 
 type notations =
     (Vernacexpr.lstring * Constrexpr.constr_expr * Notation_term.scope_name option) list
@@ -84,7 +84,7 @@ val add_mutual_definitions :
   ?tactic:unit Proofview.tactic ->
   ?kind:Decl_kinds.definition_kind ->
   ?reduce:(Term.constr -> Term.constr) ->
-  ?hook:unit Lemmas.declaration_hook -> ?opaque:bool ->
+  ?hook:(Evd.evar_universe_context -> unit) Lemmas.declaration_hook -> ?opaque:bool ->
   notations ->
   fixpoint_kind -> unit