[declareDef] More consistent handling of universe binders

The only reasons that `prepare_definition` returned a sigma were:
- to obtain the universe binders to be passed to declare
- to obtain the UState.t to be passed to the equations hook

We handle this automatically now; it seems like a reasonably good API
improvement.

However, it is not clear what we do now is right for all cases; must
check.

9 files changed, 51 insertions, 66 deletions

diff --git a/doc/plugin_tutorial/tuto1/src/simple_declare.ml b/doc/plugin_tutorial/tuto1/src/simple_declare.ml
index 3b906324f4..a2783d80e8 100644
--- a/doc/plugin_tutorial/tuto1/src/simple_declare.ml
+++ b/doc/plugin_tutorial/tuto1/src/simple_declare.ml
@@ -1,10 +1,7 @@
 let edeclare ?hook ~name ~poly ~scope ~kind ~opaque ~udecl ~impargs sigma body tyopt  =
-  let sigma, ce = DeclareDef.prepare_definition
+  let ce = DeclareDef.prepare_definition
       ~opaque ~poly sigma ~udecl ~types:tyopt ~body in
-  let uctx = Evd.evar_universe_context sigma in
-  let ubind = Evd.universe_binders sigma in
-  let hook_data = Option.map (fun hook -> hook, uctx, []) hook in
-  DeclareDef.declare_definition ~name ~scope ~kind ~ubind ce ~impargs ?hook_data
+  DeclareDef.declare_definition ~name ~scope ~kind ~impargs ?hook ce
 
 let declare_definition ~poly name sigma body =
   let udecl = UState.default_univ_decl in
diff --git a/plugins/funind/gen_principle.ml b/plugins/funind/gen_principle.ml
index 47e56b81aa..ebd280ecf6 100644
--- a/plugins/funind/gen_principle.ml
+++ b/plugins/funind/gen_principle.ml
@@ -290,13 +290,11 @@ let generate_functional_principle (evd: Evd.evar_map ref)
      Don't forget to close the goal if an error is raised !!!!
   *)
   let uctx = Evd.evar_universe_context sigma in
-  let hook_data = hook, uctx, [] in
-  let entry = DeclareDef.ClosedDef.of_proof_entry entry in
+  let entry = DeclareDef.ClosedDef.of_proof_entry ~uctx entry in
   let _ : Names.GlobRef.t = DeclareDef.declare_definition
-      ~name:new_princ_name ~hook_data
+      ~name:new_princ_name ~hook
       ~scope:(DeclareDef.Global Declare.ImportDefaultBehavior)
       ~kind:Decls.(IsProof Theorem)
-      ~ubind:UnivNames.empty_binders
       ~impargs:[]
       entry in
   ()
diff --git a/vernac/classes.ml b/vernac/classes.ml
index 88b6ab34ff..a882f6db0a 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -313,11 +313,10 @@ let instance_hook info global ?hook cst =
 
 let declare_instance_constant info global impargs ?hook name udecl poly sigma term termtype =
   let kind = Decls.(IsDefinition Instance) in
-  let sigma, entry = DeclareDef.prepare_definition
+  let entry = DeclareDef.prepare_definition
       ~poly sigma ~udecl ~types:(Some termtype) ~body:term in
-  let ubind = Evd.universe_binders sigma in
   let scope = DeclareDef.Global Declare.ImportDefaultBehavior in
-  let kn = DeclareDef.declare_definition ~name ~kind ~scope ~ubind ~impargs entry in
+  let kn = DeclareDef.declare_definition ~name ~kind ~scope ~impargs entry in
   instance_hook info global ?hook kn
 
 let do_declare_instance sigma ~global ~poly k u ctx ctx' pri udecl impargs subst name =
diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml
index cb9acda770..4a82696ea6 100644
--- a/vernac/comAssumption.ml
+++ b/vernac/comAssumption.ml
@@ -204,9 +204,10 @@ let context_insection sigma ~poly ctx =
         in
         let entry = Declare.definition_entry ~univs ~types:t b in
         (* XXX Fixme: Use DeclareDef.prepare_definition *)
-        let entry = DeclareDef.ClosedDef.of_proof_entry entry in
+        let uctx = Evd.evar_universe_context sigma in
+        let entry = DeclareDef.ClosedDef.of_proof_entry ~uctx entry in
         let _ : GlobRef.t = DeclareDef.declare_definition ~name ~scope:DeclareDef.Discharge
-            ~kind:Decls.(IsDefinition Definition) ~ubind:UnivNames.empty_binders ~impargs:[] entry
+            ~kind:Decls.(IsDefinition Definition) ~impargs:[] entry
         in
         ()
     in
diff --git a/vernac/comDefinition.ml b/vernac/comDefinition.ml
index 73b523f0b3..bf4567e57f 100644
--- a/vernac/comDefinition.ml
+++ b/vernac/comDefinition.ml
@@ -74,13 +74,10 @@ let do_definition ?hook ~name ~scope ~poly ~kind udecl bl red_option c ctypopt =
   let (body, types), evd, udecl, impargs =
     interp_definition ~program_mode udecl bl ~poly red_option c ctypopt
   in
-  let evd, ce = DeclareDef.prepare_definition ~opaque:false ~poly evd ~udecl ~types ~body in
-  let uctx = Evd.evar_universe_context evd in
-  let hook_data = Option.map (fun hook -> hook, uctx, []) hook in
+  let ce = DeclareDef.prepare_definition ~opaque:false ~poly evd ~udecl ~types ~body in
   let kind = Decls.IsDefinition kind in
-  let ubind = Evd.universe_binders evd in
   let _ : Names.GlobRef.t =
-    DeclareDef.declare_definition ~name ~scope ~kind ?hook_data ~ubind ~impargs ce
+    DeclareDef.declare_definition ~name ~scope ~kind ?hook ~impargs ce
   in ()
 
 let do_definition_program ?hook ~name ~scope ~poly ~kind udecl bl red_option c ctypopt =
diff --git a/vernac/declareDef.ml b/vernac/declareDef.ml
index 84310cba65..14d3daf453 100644
--- a/vernac/declareDef.ml
+++ b/vernac/declareDef.ml
@@ -9,7 +9,6 @@
 (************************************************************************)
 
 open Declare
-open Impargs
 
 type locality = Discharge | Global of Declare.import_status
 
@@ -40,40 +39,40 @@ end
 
 module ClosedDef = struct
 
-  type t = Evd.side_effects Declare.proof_entry
+  type t =
+    { entry : Evd.side_effects Declare.proof_entry
+    ; uctx : UState.t
+    }
 
-  let of_proof_entry x = x
+  let of_proof_entry ~uctx entry = { entry; uctx }
 end
 
 (* Locality stuff *)
-let declare_definition ~name ~scope ~kind ?hook_data ~ubind ~impargs ce =
-  let should_suggest = ce.Declare.proof_entry_opaque &&
-                       Option.is_empty ce.Declare.proof_entry_secctx in
+let declare_definition ~name ~scope ~kind ?hook ?(obls=[]) ~impargs ce =
+  let { ClosedDef.entry; uctx } = ce in
+  let should_suggest = entry.Declare.proof_entry_opaque &&
+                       Option.is_empty entry.Declare.proof_entry_secctx in
+  let ubind = UState.universe_binders uctx in
   let dref = match scope with
   | Discharge ->
-    let () = declare_variable ~name ~kind (SectionLocalDef ce) in
+    let () = declare_variable ~name ~kind (SectionLocalDef entry) in
     if should_suggest then Proof_using.suggest_variable (Global.env ()) name;
     Names.GlobRef.VarRef name
   | Global local ->
-    let kn = declare_constant ~name ~local ~kind (DefinitionEntry ce) in
+    let kn = declare_constant ~name ~local ~kind (DefinitionEntry entry) in
     let gr = Names.GlobRef.ConstRef kn in
     if should_suggest then Proof_using.suggest_constant (Global.env ()) kn;
     let () = DeclareUniv.declare_univ_binders gr ubind in
     gr
   in
-  let () = maybe_declare_manual_implicits false dref impargs in
+  let () = Impargs.maybe_declare_manual_implicits false dref impargs in
   let () = definition_message name in
-  begin
-    match hook_data with
-    | None -> ()
-    | Some (hook, uctx, obls) ->
-      Hook.call ~hook { Hook.S.uctx; obls; scope; dref }
-  end;
+  Option.iter (fun hook -> Hook.call ~hook { Hook.S.uctx; obls; scope; dref }) hook;
   dref
 
-let declare_definition ~name ~scope ~kind ?hook_data ~ubind ~impargs ce =
-  let fix_exn = Declare.Internal.get_fix_exn ce in
-  try declare_definition ~name ~scope ~kind ?hook_data ~ubind ~impargs ce
+let declare_definition ~name ~scope ~kind ?hook ?obls ~impargs ce =
+  let fix_exn = Declare.Internal.get_fix_exn ce.ClosedDef.entry in
+  try declare_definition ~name ~scope ~kind ?hook ?obls ~impargs ce
   with exn ->
     let exn = Exninfo.capture exn in
     Exninfo.iraise (fix_exn exn)
@@ -107,22 +106,21 @@ end
 let declare_mutually_recursive ~opaque ~scope ~kind ~poly ~uctx ~udecl ~ntns ~rec_declaration ~possible_indexes ?(restrict_ucontext=true) fixitems =
   let vars, fixdecls, indexes =
     mutual_make_bodies ~fixitems ~rec_declaration ~possible_indexes in
-  let ubind, univs =
+  let uctx, univs =
     (* XXX: Obligations don't do this, this seems like a bug? *)
     if restrict_ucontext
     then
-      let evd = Evd.from_ctx uctx in
-      let evd = Evd.restrict_universe_context evd vars in
-      let univs = Evd.check_univ_decl ~poly evd udecl in
-      Evd.universe_binders evd, univs
+      let uctx = UState.restrict uctx vars in
+      let univs = UState.check_univ_decl ~poly uctx udecl in
+      uctx, univs
     else
       let univs = UState.univ_entry ~poly uctx in
-      UnivNames.empty_binders, univs
+      uctx, univs
   in
   let csts = CList.map2
       (fun Recthm.{ name; typ; impargs } body ->
-         let ce = Declare.definition_entry ~opaque ~types:typ ~univs body in
-         declare_definition ~name ~scope ~kind ~ubind ~impargs ce)
+         let entry = Declare.definition_entry ~opaque ~types:typ ~univs body in
+         declare_definition ~name ~scope ~kind ~impargs { ClosedDef.entry; uctx })
       fixitems fixdecls
   in
   let isfix = Option.is_empty possible_indexes in
@@ -167,7 +165,9 @@ let prepare_definition ?opaque ?inline ?fix_exn ~poly ~udecl ~types ~body sigma
       sigma (fun nf -> nf body, Option.map nf types)
   in
   let univs = Evd.check_univ_decl ~poly sigma udecl in
-  sigma, definition_entry ?fix_exn ?opaque ?inline ?types ~univs body
+  let entry = definition_entry ?fix_exn ?opaque ?inline ?types ~univs body in
+  let uctx = Evd.evar_universe_context sigma in
+  { ClosedDef.entry; uctx }
 
 let prepare_obligation ?opaque ?inline ~name ~poly ~udecl ~types ~body sigma =
   let sigma, (body, types) = Evarutil.finalize ~abort_on_undefined_evars:false
diff --git a/vernac/declareDef.mli b/vernac/declareDef.mli
index 9c5cd6fc2a..8f3db59ba9 100644
--- a/vernac/declareDef.mli
+++ b/vernac/declareDef.mli
@@ -43,15 +43,17 @@ module ClosedDef : sig
   type t
 
   (* Don't use for non-interactive proofs *)
-  val of_proof_entry : Evd.side_effects Declare.proof_entry -> t
+  val of_proof_entry
+    : uctx:UState.t
+    -> Evd.side_effects Declare.proof_entry -> t
 end
 
 val declare_definition
   :  name:Id.t
   -> scope:locality
   -> kind:Decls.logical_kind
-  -> ?hook_data:(Hook.t * UState.t * (Id.t * Constr.t) list)
-  -> ubind:UnivNames.universe_binders
+  -> ?hook:Hook.t
+  -> ?obls:(Id.t * Constr.t) list
   -> impargs:Impargs.manual_implicits
   -> ClosedDef.t
   -> GlobRef.t
@@ -95,9 +97,6 @@ val declare_mutually_recursive
   -> Recthm.t list
   -> Names.GlobRef.t list
 
-(* The common use of the returned evar_map is to obtain the universe
-   binders and context for the hook; we should refactor that soon by
-   merging prepare and declare. *)
 val prepare_definition
   :  ?opaque:bool
   -> ?inline:bool
@@ -107,7 +106,7 @@ val prepare_definition
   -> types:EConstr.t option
   -> body:EConstr.t
   -> Evd.evar_map
-  -> Evd.evar_map * ClosedDef.t
+  -> ClosedDef.t
 
 val prepare_obligation
   :  ?opaque:bool
diff --git a/vernac/declareObl.ml b/vernac/declareObl.ml
index f9d842d6a7..4c62582c23 100644
--- a/vernac/declareObl.ml
+++ b/vernac/declareObl.ml
@@ -365,20 +365,15 @@ let declare_definition prg =
   let sigma = Evd.from_ctx prg.prg_ctx in
   let body, types = subst_prog varsubst prg in
   let body, types = EConstr.(of_constr body, Some (of_constr types)) in
-  let opaque, poly, udecl = prg.prg_opaque, prg.prg_poly, prg.prg_univdecl in
+  (* All these should be grouped into a struct a some point *)
+  let opaque, poly, udecl, hook = prg.prg_opaque, prg.prg_poly, prg.prg_univdecl, prg.prg_hook in
+  let name, scope, kind, impargs = prg.prg_name, prg.prg_scope, Decls.(IsDefinition prg.prg_kind), prg.prg_implicits in
   let fix_exn = Hook.get get_fix_exn () in
   let obls = List.map (fun (id, (_, c)) -> (id, c)) varsubst in
   (* XXX: This is doing normalization twice *)
-  let sigma, ce =
-    DeclareDef.prepare_definition ~fix_exn ~opaque ~poly ~udecl ~types ~body sigma in
+  let ce = DeclareDef.prepare_definition ~fix_exn ~opaque ~poly ~udecl ~types ~body sigma in
   let () = progmap_remove prg in
-  let uctx = Evd.evar_universe_context sigma in
-  let ubind = UState.universe_binders uctx in
-  let hook_data = Option.map (fun hook -> hook, uctx, obls) prg.prg_hook in
-  DeclareDef.declare_definition
-    ~name:prg.prg_name ~scope:prg.prg_scope ~ubind
-    ~kind:Decls.(IsDefinition prg.prg_kind) ce
-    ~impargs:prg.prg_implicits ?hook_data
+  DeclareDef.declare_definition ~name ~scope ~kind ~impargs ?hook ~obls ce
 
 let rec lam_index n t acc =
   match Constr.kind t with
diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index a1bcf95bf5..042fdd6885 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -233,7 +233,6 @@ end = struct
       then Declare.Internal.map_entry_type pe ~f:(fun _ -> Some typ), UnivNames.empty_binders
       else pe, UState.universe_binders uctx
     in
-    let hook_data = Option.map (fun hook -> hook, uctx, []) info.Info.hook in
     (* We when compute_guard was [] in the previous step we should not
        substitute the body *)
     let pe = match compute_guard with
@@ -242,8 +241,8 @@ end = struct
         Declare.Internal.map_entry_body pe
           ~f:(fun ((body, ctx), eff) -> (select_body i body, ctx), eff)
     in
-    let pe = DeclareDef.ClosedDef.of_proof_entry pe in
-    DeclareDef.declare_definition ~name ~scope ~kind ?hook_data ~ubind ~impargs pe
+    let pe = DeclareDef.ClosedDef.of_proof_entry ~uctx pe in
+    DeclareDef.declare_definition ~name ~scope ~kind ?hook ~impargs pe
 
   let declare_mutdef ~info ~uctx const =
     let pe = match info.Info.compute_guard with