Cleanup API for registering universe binders.

- Regularly declared for for polymorphic constants
- Declared globally for monomorphic constants.

  E.g mono@{i} := Type@{i} is printed as
  mono@{mono.i} := Type@{mono.i}.

  There can be a name clash if there's a module and a constant of the
  same name. It is detected and is an error if the constant is first
  but is not detected and the name for the constant not
  registered (??) if the constant comes second.

Accept VarRef when registering universe binders

Fix two problems found by Gaëtan where binders were not registered properly

Simplify API substantially by not passing around a substructure of an
already carrier-around structure in interpretation/declaration code of
constants and proofs

Fix an issue of the stronger restrict universe context + no evd leak

This is uncovered by not having an evd leak in interp_definition, and
the stronger restrict_universe_context. This patch could be backported
to 8.7, it could also be triggered by the previous restrict_context I
think.

19 files changed, 233 insertions, 103 deletions

diff --git a/API/API.mli b/API/API.mli
index 9d1585d60..6227f17c6 100644
--- a/API/API.mli
+++ b/API/API.mli
@@ -4847,17 +4847,16 @@ sig
       set : unit -> unit ;
       reset : unit -> unit
     }
-  type proof_universes = UState.t * Universes.universe_binders option
   type proof_object = {
     id : Names.Id.t;
     entries : Safe_typing.private_constants Entries.definition_entry list;
     persistence : Decl_kinds.goal_kind;
-    universes: proof_universes;
+    universes: UState.t;
   }
 
   type proof_ending =
   | Admitted of Names.Id.t * Decl_kinds.goal_kind * Entries.parameter_entry *
-                  proof_universes
+                  UState.t
   | Proved of Vernacexpr.opacity_flag *
               Vernacexpr.lident option *
               proof_object
@@ -5011,7 +5010,7 @@ sig
       Vernacexpr.goal_selector -> int option -> unit Proofview.tactic ->
       Proof.t -> Proof.t * bool
   val cook_proof :
-    unit -> (Names.Id.t * (Safe_typing.private_constants Entries.definition_entry * Proof_global.proof_universes * Decl_kinds.goal_kind))
+    unit -> (Names.Id.t * (Safe_typing.private_constants Entries.definition_entry * UState.t * Decl_kinds.goal_kind))
 
   val get_current_context : unit -> Evd.evar_map * Environ.env
   val current_proof_statement : unit -> Names.Id.t * Decl_kinds.goal_kind * EConstr.types
diff --git a/engine/eConstr.ml b/engine/eConstr.ml
index afdceae06..ea098902a 100644
--- a/engine/eConstr.ml
+++ b/engine/eConstr.ml
@@ -645,6 +645,24 @@ let eq_constr_universes_proj env sigma m n =
     let res = eq_constr' (unsafe_to_constr m) (unsafe_to_constr n) in
     if res then Some !cstrs else None
 
+let universes_of_constr sigma c =
+  let open Univ in
+  let rec aux s c =
+    match kind sigma c with
+    | Const (_, u) | Ind (_, u) | Construct (_, u) ->
+      LSet.fold LSet.add (Instance.levels (EInstance.kind sigma u)) s
+    | Sort u ->
+       let sort = ESorts.kind sigma u in
+       if Sorts.is_small sort then s
+       else
+         let u = Sorts.univ_of_sort sort in
+         LSet.fold LSet.add (Universe.levels u) s
+    | Evar (k, args) ->
+       let concl = Evd.evar_concl (Evd.find sigma k) in
+       fold sigma aux (aux s (of_constr concl)) c
+    | _ -> fold sigma aux s c
+  in aux LSet.empty c
+
 open Context
 open Environ
 
diff --git a/engine/eConstr.mli b/engine/eConstr.mli
index e9ef302cf..3e6a13f70 100644
--- a/engine/eConstr.mli
+++ b/engine/eConstr.mli
@@ -201,6 +201,10 @@ val iter_with_binders : Evd.evar_map -> ('a -> 'a) -> ('a -> t -> unit) -> 'a ->
 val iter_with_full_binders : Evd.evar_map -> (rel_declaration -> 'a -> 'a) -> ('a -> t -> unit) -> 'a -> t -> unit
 val fold : Evd.evar_map -> ('a -> t -> 'a) -> 'a -> t -> 'a
 
+(** Gather the universes transitively used in the term, including in the
+   type of evars appearing in it. *)
+val universes_of_constr : Evd.evar_map -> t -> Univ.LSet.t
+
 (** {6 Substitutions} *)
 
 module Vars :
diff --git a/interp/declare.ml b/interp/declare.ml
index 8fc959b0f..1aeb67afb 100644
--- a/interp/declare.ml
+++ b/interp/declare.ml
@@ -458,33 +458,61 @@ let declare_universe_context poly ctx =
    used to distinguish universes declared in polymorphic sections, which
    are discharged and do not remain in scope. *)
 
-type universe_decl = polymorphic * Nametab.universe_id
+type universe_source =
+  | BoundUniv (* polymorphic universe, bound in a function (this will go away someday) *)
+  | QualifiedUniv of Id.t (* global universe introduced by some global value *)
+  | UnqualifiedUniv (* other global universe *)
 
-let add_universe p (dp, i) =
+type universe_decl = universe_source * Nametab.universe_id
+
+let add_universe src (dp, i) =
   let level = Univ.Level.make dp i in
-  let ctx = Univ.ContextSet.add_universe level Univ.ContextSet.empty in
-  Global.push_context_set p ctx;
-  Universes.add_global_universe level p;
-  if p then Lib.add_section_context ctx
+  let optpoly = match src with
+    | BoundUniv -> Some true
+    | UnqualifiedUniv -> Some false
+    | QualifiedUniv _ -> None
+  in
+  Option.iter (fun poly ->
+      let ctx = Univ.ContextSet.add_universe level Univ.ContextSet.empty in
+      Global.push_context_set poly ctx;
+      Universes.add_global_universe level poly;
+      if poly then Lib.add_section_context ctx)
+    optpoly
 
 let check_exists sp =
   let depth = sections_depth () in
   let sp = Libnames.make_path (pop_dirpath_n depth (dirpath sp)) (basename sp) in
-  if Nametab.exists_universe sp then alreadydeclared (Id.print (basename sp) ++ str " already exists")
+  if Nametab.exists_universe sp then
+    alreadydeclared (str "Universe " ++ Id.print (basename sp) ++ str " already exists")
   else ()
 
-let cache_universe ((sp, _), (poly, id)) =
+let qualify_univ src (sp,i as orig) =
+  match src with
+  | BoundUniv | UnqualifiedUniv -> orig
+  | QualifiedUniv l ->
+    let sp0, id = Libnames.repr_path sp in
+    let sp0 = DirPath.repr sp0 in
+    Libnames.make_path (DirPath.make (l::sp0)) id, i+1
+
+let cache_universe ((sp, _), (src, id)) =
+  let sp, i = qualify_univ src (sp,1) in
   let () = check_exists sp in
-  let () = Nametab.push_universe (Nametab.Until 1) sp id in
-    add_universe poly id
+  let () = Nametab.push_universe (Nametab.Until i) sp id in
+    add_universe src id
 
-let load_universe i ((sp, _), (poly, id)) =
+let load_universe i ((sp, _), (src, id)) =
+  let sp, i = qualify_univ src (sp,i) in
   let () = Nametab.push_universe (Nametab.Until i) sp id in
-  add_universe poly id
+  add_universe src id
 
-let open_universe i ((sp, _), (poly, id)) =
+let open_universe i ((sp, _), (src, id)) =
+  let sp, i = qualify_univ src (sp,i) in
   let () = Nametab.push_universe (Nametab.Exactly i) sp id in
-  ()(** add_universe p id Necessary ? *)
+  ()
+
+let discharge_universe = function
+  | _, (BoundUniv, _) -> None
+  | _, ((QualifiedUniv _ | UnqualifiedUniv), _ as x) -> Some x
 
 let input_universe : universe_decl -> Libobject.obj =
   declare_object
@@ -492,12 +520,28 @@ let input_universe : universe_decl -> Libobject.obj =
       cache_function = cache_universe;
       load_function = load_universe;
       open_function = open_universe;
-      discharge_function = (fun (_, (p, _ as x)) -> if p then None else Some x);
+      discharge_function = discharge_universe;
       subst_function = (fun (subst, a) -> (** Actually the name is generated once and for all. *) a);
       classify_function = (fun a -> Substitute a) }
 
-let add_universe poly (id, lev) =
-  ignore(Lib.add_leaf id (input_universe (poly, lev)))
+let declare_univ_binders gr pl =
+  if Global.is_polymorphic gr then
+    Universes.register_universe_binders gr pl
+  else
+    let l = match gr with
+      | ConstRef c -> Label.to_id @@ Constant.label c
+      | IndRef (c, _) -> Label.to_id @@ MutInd.label c
+      | VarRef id -> id
+      | ConstructRef _ ->
+        anomaly ~label:"declare_univ_binders"
+          Pp.(str "declare_univ_binders on an constructor reference")
+    in
+    Id.Map.iter (fun id lvl ->
+        match Univ.Level.name lvl with
+        | None -> ()
+        | Some na ->
+          ignore (Lib.add_leaf id (input_universe (QualifiedUniv l, na))))
+      pl
 
 let do_universe poly l =
   let in_section = Lib.sections_are_opened () in
@@ -511,7 +555,10 @@ let do_universe poly l =
       let lev = Universes.new_univ_id () in
       (id, lev)) l
   in
-  List.iter (add_universe poly) l
+  let src = if poly then BoundUniv else UnqualifiedUniv in
+  List.iter (fun (id,lev) ->
+      ignore(Lib.add_leaf id (input_universe (src, lev))))
+    l
 
 type constraint_decl = polymorphic * Univ.constraints
 
diff --git a/interp/declare.mli b/interp/declare.mli
index 31883c9d7..f368d164e 100644
--- a/interp/declare.mli
+++ b/interp/declare.mli
@@ -80,9 +80,8 @@ val recursive_message : bool (** true = fixpoint *) ->
 
 val exists_name : Id.t -> bool
 
-
-
 (** Global universe contexts, names and constraints *)
+val declare_univ_binders : Globnames.global_reference -> Universes.universe_binders -> unit
 
 val declare_universe_context : polymorphic -> Univ.ContextSet.t -> unit
 
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index c526ae000..31a73db04 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -140,7 +140,7 @@ let build_constant_by_tactic id ctx sign ?(goal_kind = Global, false, Proof Theo
     let status = by tac in
     let _,(const,univs,_) = cook_proof () in
     Proof_global.discard_current ();
-    const, status, fst univs
+    const, status, univs
   with reraise ->
     let reraise = CErrors.push reraise in
     Proof_global.discard_current ();
diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli
index 2acb678d7..5a317a956 100644
--- a/proofs/pfedit.mli
+++ b/proofs/pfedit.mli
@@ -35,11 +35,11 @@ val start_proof :
 val cook_this_proof :
     Proof_global.proof_object ->
   (Id.t *
-    (Safe_typing.private_constants Entries.definition_entry * Proof_global.proof_universes * goal_kind))
+    (Safe_typing.private_constants Entries.definition_entry * UState.t * goal_kind))
 
 val cook_proof : unit ->
   (Id.t *
-    (Safe_typing.private_constants Entries.definition_entry * Proof_global.proof_universes * goal_kind))
+    (Safe_typing.private_constants Entries.definition_entry * UState.t * goal_kind))
 
 (** {6 ... } *)
 (** [get_goal_context n] returns the context of the [n]th subgoal of
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index c1e1c2eda..535ef2013 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -68,17 +68,16 @@ let _ =
 
 (* Extra info on proofs. *)
 type lemma_possible_guards = int list list
-type proof_universes = UState.t * Universes.universe_binders option
 
 type proof_object = {
   id : Names.Id.t;
   entries : Safe_typing.private_constants Entries.definition_entry list;
   persistence : Decl_kinds.goal_kind;
-  universes: proof_universes;
+  universes: UState.t;
 }
 
 type proof_ending =
-  | Admitted of Names.Id.t * Decl_kinds.goal_kind * Entries.parameter_entry * proof_universes
+  | Admitted of Names.Id.t * Decl_kinds.goal_kind * Entries.parameter_entry * UState.t
   | Proved of Vernacexpr.opacity_flag *
               Vernacexpr.lident option *
               proof_object
@@ -333,7 +332,6 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now
   in
   let fpl, univs = Future.split2 fpl in
   let universes = if poly || now then Future.force univs else initial_euctx in
-  let binders = if poly then Some (UState.universe_binders universes) else None in
   (* Because of dependent subgoals at the beginning of proofs, we could
      have existential variables in the initial types of goals, we need to
      normalise them for the kernel. *)
@@ -409,7 +407,7 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now
   in
   let entries = Future.map2 entry_fn fpl initial_goals in
   { id = pid; entries = entries; persistence = strength;
-    universes = (universes, binders) },
+    universes },
   fun pr_ending -> CEphemeron.get terminator pr_ending
 
 let return_proof ?(allow_partial=false) () =
diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli
index 059459042..27e99f218 100644
--- a/proofs/proof_global.mli
+++ b/proofs/proof_global.mli
@@ -37,18 +37,17 @@ val compact_the_proof : unit -> unit
     (i.e. an proof ending command) and registers the appropriate
     values. *)
 type lemma_possible_guards = int list list
-type proof_universes = UState.t * Universes.universe_binders option
 
 type proof_object = {
   id : Names.Id.t;
   entries : Safe_typing.private_constants Entries.definition_entry list;
   persistence : Decl_kinds.goal_kind;
-  universes: proof_universes;
+  universes: UState.t;
 }
 
 type proof_ending =
   | Admitted of Names.Id.t * Decl_kinds.goal_kind * Entries.parameter_entry *
-		  proof_universes
+                UState.t
   | Proved of Vernacexpr.opacity_flag *
               Vernacexpr.lident option *
               proof_object
diff --git a/test-suite/output/UnivBinders.out b/test-suite/output/UnivBinders.out
index f69379a57..d6d410d1a 100644
--- a/test-suite/output/UnivBinders.out
+++ b/test-suite/output/UnivBinders.out
@@ -44,26 +44,45 @@ bar@{u} = nat
 bar is universe polymorphic
 foo@{u Top.17 v} = 
 Type@{Top.17} -> Type@{v} -> Type@{u}
-     : Type@{max(u+1, Top.17+1, v+1)}
+     : Type@{max(u+1,Top.17+1,v+1)}
 (* u Top.17 v |=  *)
 
 foo is universe polymorphic
-Monomorphic mono = Type@{u}
-     : Type@{u+1}
-(* {u} |=  *)
+Monomorphic mono = Type@{mono.u}
+     : Type@{mono.u+1}
+(* {mono.u} |=  *)
 
 mono is not universe polymorphic
+mono
+     : Type@{mono.u+1}
+Type@{mono.u}
+     : Type@{mono.u+1}
+The command has indeed failed with message:
+Universe u already exists.
+monomono
+     : Type@{MONOU+1}
+mono.monomono
+     : Type@{mono.MONOU+1}
+monomono
+     : Type@{MONOU+1}
+mono
+     : Type@{mono.u+1}
+The command has indeed failed with message:
+Universe u already exists.
+bobmorane = 
+let tt := Type@{tt.v} in let ff := Type@{ff.v} in tt -> ff
+     : Type@{max(tt.u,ff.u)}
 The command has indeed failed with message:
 Universe u already bound.
 foo@{E M N} = 
 Type@{M} -> Type@{N} -> Type@{E}
-     : Type@{max(E+1, M+1, N+1)}
+     : Type@{max(E+1,M+1,N+1)}
 (* E M N |=  *)
 
 foo is universe polymorphic
 foo@{Top.16 Top.17 Top.18} = 
 Type@{Top.17} -> Type@{Top.18} -> Type@{Top.16}
-     : Type@{max(Top.16+1, Top.17+1, Top.18+1)}
+     : Type@{max(Top.16+1,Top.17+1,Top.18+1)}
 (* Top.16 Top.17 Top.18 |=  *)
 
 foo is universe polymorphic
@@ -88,9 +107,10 @@ The command has indeed failed with message:
 This object does not support universe names.
 The command has indeed failed with message:
 Cannot enforce v < u because u < gU < gV < v
-Monomorphic bind_univs.mono = Type@{u}
-     : Type@{u+1}
-(* {u} |=  *)
+Monomorphic bind_univs.mono = 
+Type@{bind_univs.mono.u}
+     : Type@{bind_univs.mono.u+1}
+(* {bind_univs.mono.u} |=  *)
 
 bind_univs.mono is not universe polymorphic
 bind_univs.poly@{u} = Type@{u}
@@ -99,12 +119,12 @@ bind_univs.poly@{u} = Type@{u}
 
 bind_univs.poly is universe polymorphic
 insec@{v} = Type@{u} -> Type@{v}
-     : Type@{max(u+1, v+1)}
+     : Type@{max(u+1,v+1)}
 (* v |=  *)
 
 insec is universe polymorphic
 insec@{u v} = Type@{u} -> Type@{v}
-     : Type@{max(u+1, v+1)}
+     : Type@{max(u+1,v+1)}
 (* u v |=  *)
 
 insec is universe polymorphic
@@ -125,28 +145,28 @@ inmod@{u} = Type@{u}
 inmod is universe polymorphic
 Applied.infunct@{u v} = 
 inmod@{u} -> Type@{v}
-     : Type@{max(u+1, v+1)}
+     : Type@{max(u+1,v+1)}
 (* u v |=  *)
 
 Applied.infunct is universe polymorphic
-axfoo@{i Top.33 Top.34} : Type@{Top.33} -> Type@{i}
-(* i Top.33 Top.34 |=  *)
+axfoo@{i Top.41 Top.42} : Type@{Top.41} -> Type@{i}
+(* i Top.41 Top.42 |=  *)
 
 axfoo is universe polymorphic
 Argument scope is [type_scope]
 Expands to: Constant Top.axfoo
-axbar@{i Top.33 Top.34} : Type@{Top.34} -> Type@{i}
-(* i Top.33 Top.34 |=  *)
+axbar@{i Top.41 Top.42} : Type@{Top.42} -> Type@{i}
+(* i Top.41 Top.42 |=  *)
 
 axbar is universe polymorphic
 Argument scope is [type_scope]
 Expands to: Constant Top.axbar
-axfoo' : Type@{Top.36} -> Type@{i}
+axfoo' : Type@{Top.44} -> Type@{axbar'.i}
 
 axfoo' is not universe polymorphic
 Argument scope is [type_scope]
 Expands to: Constant Top.axfoo'
-axbar' : Type@{Top.36} -> Type@{i}
+axbar' : Type@{Top.44} -> Type@{axbar'.i}
 
 axbar' is not universe polymorphic
 Argument scope is [type_scope]
diff --git a/test-suite/output/UnivBinders.v b/test-suite/output/UnivBinders.v
index 116d5e5e9..266d94ad9 100644
--- a/test-suite/output/UnivBinders.v
+++ b/test-suite/output/UnivBinders.v
@@ -1,6 +1,6 @@
 Set Universe Polymorphism.
 Set Printing Universes.
-Unset Strict Universe Declaration.
+(* Unset Strict Universe Declaration. *)
 
 (* universe binders on inductive types and record projections *)
 Inductive Empty@{u} : Type@{u} := .
@@ -25,14 +25,59 @@ Print wrap.
 Instance bar@{u} : Wrap@{u} Set. Proof. exact nat. Qed.
 Print bar.
 
+Unset Strict Universe Declaration.
 (* The universes in the binder come first, then the extra universes in
    order of appearance. *)
 Definition foo@{u +} := Type -> Type@{v} -> Type@{u}.
 Print foo.
+Set Strict Universe Declaration.
 
 (* Binders even work with monomorphic definitions! *)
 Monomorphic Definition mono@{u} := Type@{u}.
 Print mono.
+Check mono.
+Check Type@{mono.u}.
+
+Module mono.
+  Fail Monomorphic Universe u.
+  Monomorphic Universe MONOU.
+
+  Monomorphic Definition monomono := Type@{MONOU}.
+  Check monomono.
+End mono.
+Check mono.monomono. (* qualified MONOU *)
+Import mono.
+Check monomono. (* unqualified MONOU *)
+Check mono. (* still qualified mono.u *)
+
+Monomorphic Constraint Set < Top.mono.u.
+
+Module mono2.
+  Monomorphic Universe u.
+End mono2.
+
+Fail Monomorphic Definition mono2@{u} := Type@{u}.
+
+Module SecLet.
+  Unset Universe Polymorphism.
+  Section foo.
+    (* Fail Let foo@{} := Type@{u}. (* doesn't parse: Let foo@{...} doesn't exist *) *)
+    Unset Strict Universe Declaration.
+    Let tt : Type@{u} := Type@{v}. (* names disappear in the ether *)
+    Let ff : Type@{u}. Proof. exact Type@{v}. Qed. (* if Set Universe Polymorphism: universes are named ff.u and ff.v. Otherwise names disappear into space *)
+    Definition bobmorane := tt -> ff.
+  End foo.
+  Print bobmorane. (*
+                     bobmorane@{Top.15 Top.16 ff.u ff.v} =
+                     let tt := Type@{Top.16} in let ff := Type@{ff.v} in tt -> ff
+                     : Type@{max(Top.15,ff.u)}
+                     (* Top.15 Top.16 ff.u ff.v |= Top.16 < Top.15
+                     ff.v < ff.u
+                    *)
+
+                    bobmorane is universe polymorphic
+                    *)
+End SecLet.
 
 (* fun x x => foo is nonsense with local binders *)
 Fail Definition fo@{u u} := Type@{u}.
@@ -61,7 +106,7 @@ Monomorphic Universes gU gV. Monomorphic Constraint gU < gV.
 Fail Lemma foo@{u v|u < gU, gV < v, v < u} : nat.
 
 (* Universe binders survive through compilation, sections and modules. *)
-Require bind_univs.
+Require TestSuite.bind_univs.
 Print bind_univs.mono.
 Print bind_univs.poly.
 
diff --git a/test-suite/prerequisite/bind_univs.v b/test-suite/prerequisite/bind_univs.v
index f17c00e9d..e834fde11 100644
--- a/test-suite/prerequisite/bind_univs.v
+++ b/test-suite/prerequisite/bind_univs.v
@@ -3,3 +3,5 @@
 Monomorphic Definition mono@{u} := Type@{u}.
 
 Polymorphic Definition poly@{u} := Type@{u}.
+
+Monomorphic Universe reqU.
diff --git a/vernac/classes.ml b/vernac/classes.ml
index b80741269..cb1d2f7c7 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -126,7 +126,7 @@ let declare_instance_constant k info global imps ?hook id decl poly evm term ter
   let cdecl = (DefinitionEntry entry, kind) in
   let kn = Declare.declare_constant id cdecl in
     Declare.definition_message id;
-    Universes.register_universe_binders (ConstRef kn) (Evd.universe_binders evm);
+    Declare.declare_univ_binders (ConstRef kn) (Evd.universe_binders evm);
     instance_hook k info global imps ?hook (ConstRef kn);
     id
 
@@ -208,7 +208,7 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance)
           (ParameterEntry
             (None,(termtype,univs),None), Decl_kinds.IsAssumption Decl_kinds.Logical)
         in
-          Universes.register_universe_binders (ConstRef cst) (Evd.universe_binders !evars);
+          Declare.declare_univ_binders (ConstRef cst) (Evd.universe_binders !evars);
           instance_hook k pri global imps ?hook (ConstRef cst); id
       end
     else (
diff --git a/vernac/command.ml b/vernac/command.ml
index 01c7f149b..66d4fe984 100644
--- a/vernac/command.ml
+++ b/vernac/command.ml
@@ -95,7 +95,7 @@ let interp_definition pl bl poly red_option c ctypopt =
   let impls, ((env_bl, ctx), imps1) = interp_context_evars env evdref bl in
   let ctx = List.map (fun d -> map_rel_decl EConstr.Unsafe.to_constr d) ctx in
   let nb_args = Context.Rel.nhyps ctx in
-  let imps,pl,ce =
+  let imps,ce =
     match ctypopt with
       None ->
         let subst = evd_comb0 Evd.nf_univ_variables evdref in
@@ -105,11 +105,10 @@ let interp_definition pl bl poly red_option c ctypopt =
 	let c = EConstr.Unsafe.to_constr c in
         let nf,subst = Evarutil.e_nf_evars_and_universes evdref in
         let body = nf (it_mkLambda_or_LetIn c ctx) in
-        let vars = Univops.universes_of_constr body in
-        let evd = Evd.restrict_universe_context !evdref vars in
-        let uctx = Evd.check_univ_decl ~poly evd decl in
-        let binders = Evd.universe_binders evd in
-        imps1@(Impargs.lift_implicits nb_args imps2), binders,
+        let vars = EConstr.universes_of_constr !evdref (EConstr.of_constr body) in
+        let () = evdref := Evd.restrict_universe_context !evdref vars in
+        let uctx = Evd.check_univ_decl ~poly !evdref decl in
+        imps1@(Impargs.lift_implicits nb_args imps2),
           definition_entry ~univs:uctx body
     | Some ctyp ->
         let ty, impsty = interp_type_evars_impls ~impls env_bl evdref ctyp in
@@ -131,23 +130,22 @@ let interp_definition pl bl poly red_option c ctypopt =
         in
 	if not (try List.for_all chk imps2 with Not_found -> false)
 	then warn_implicits_in_term ();
-        let vars = Univ.LSet.union (Univops.universes_of_constr body) 
-          (Univops.universes_of_constr typ) in
-        let ctx = Evd.restrict_universe_context !evdref vars in
-        let uctx = Evd.check_univ_decl ~poly ctx decl in
-        let binders = Evd.universe_binders evd in
-        imps1@(Impargs.lift_implicits nb_args impsty), binders,
-          definition_entry ~types:typ
-	    ~univs:uctx body
+        let bodyvars = EConstr.universes_of_constr !evdref (EConstr.of_constr body) in
+        let tyvars = EConstr.universes_of_constr !evdref (EConstr.of_constr ty) in
+        let vars = Univ.LSet.union bodyvars tyvars in
+        let () = evdref := Evd.restrict_universe_context !evdref vars in
+        let uctx = Evd.check_univ_decl ~poly !evdref decl in
+        imps1@(Impargs.lift_implicits nb_args impsty),
+          definition_entry ~types:typ ~univs:uctx body
   in
-  red_constant_entry (Context.Rel.length ctx) ce !evdref red_option, !evdref, decl, pl, imps
+  (red_constant_entry (Context.Rel.length ctx) ce !evdref red_option, !evdref, decl, imps)
 
-let check_definition (ce, evd, _, _, imps) =
+let check_definition (ce, evd, _, imps) =
   check_evars_are_solved (Global.env ()) evd Evd.empty;
   ce
 
 let do_definition ident k univdecl bl red_option c ctypopt hook =
-  let (ce, evd, univdecl, pl', imps as def) =
+  let (ce, evd, univdecl, imps as def) =
     interp_definition univdecl bl (pi2 k) red_option c ctypopt
   in
     if Flags.is_program_mode () then
@@ -168,7 +166,7 @@ let do_definition ident k univdecl bl red_option c ctypopt hook =
       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 pl' imps
+      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)))
 
@@ -224,7 +222,7 @@ match local with
   let kn = declare_constant ident ~local decl in
   let gr = ConstRef kn in
   let () = maybe_declare_manual_implicits false gr imps in
-  let () = Universes.register_universe_binders gr pl in
+  let () = Declare.declare_univ_binders gr pl in
   let () = assumption_message ident in
   let () = if do_instance then Typeclasses.declare_instance None false gr in
   let () = if is_coe then Class.try_add_new_coercion gr ~local p in
@@ -712,7 +710,7 @@ let declare_mutual_inductive_with_eliminations mie pl impls =
 	      let ind = (mind,i) in
 	      let gr = IndRef ind in
 	      maybe_declare_manual_implicits false gr indimpls;
-	      Universes.register_universe_binders gr pl;
+              Declare.declare_univ_binders gr pl;
 	      List.iteri
 		(fun j impls ->
 		 maybe_declare_manual_implicits false
@@ -1268,7 +1266,7 @@ let collect_evars_of_term evd c ty =
   Evar.Set.fold (fun ev acc -> Evd.add acc ev (Evd.find_undefined evd ev))
   evars (Evd.from_ctx (Evd.evar_universe_context evd))
 
-let do_program_recursive local p fixkind fixl ntns =
+let do_program_recursive local poly fixkind fixl ntns =
   let isfix = fixkind != Obligations.IsCoFixpoint in
   let (env, rec_sign, pl, evd), fix, info = 
     interp_recursive isfix fixl ntns 
@@ -1310,8 +1308,8 @@ let do_program_recursive local p fixkind fixl ntns =
   end in
   let ctx = Evd.evar_universe_context evd in
   let kind = match fixkind with
-  | Obligations.IsFixpoint _ -> (local, p, Fixpoint)
-  | Obligations.IsCoFixpoint -> (local, p, CoFixpoint)
+  | Obligations.IsFixpoint _ -> (local, poly, Fixpoint)
+  | Obligations.IsCoFixpoint -> (local, poly, CoFixpoint)
   in
   Obligations.add_mutual_definitions defs ~kind ~univdecl:pl ctx ntns fixkind
 
diff --git a/vernac/command.mli b/vernac/command.mli
index 070f3e112..a1f916c78 100644
--- a/vernac/command.mli
+++ b/vernac/command.mli
@@ -28,7 +28,7 @@ val do_constraint : polymorphic ->
 val interp_definition :
   Vernacexpr.universe_decl_expr option -> local_binder_expr list -> polymorphic -> red_expr option -> constr_expr ->
   constr_expr option -> Safe_typing.private_constants definition_entry * Evd.evar_map * 
-                        Univdecls.universe_decl * Universes.universe_binders * Impargs.manual_implicits
+                        Univdecls.universe_decl * Impargs.manual_implicits
 
 val do_definition : Id.t -> definition_kind -> Vernacexpr.universe_decl_expr option ->
   local_binder_expr list -> red_expr option -> constr_expr ->
diff --git a/vernac/declareDef.ml b/vernac/declareDef.ml
index 980db4109..dfac78c04 100644
--- a/vernac/declareDef.ml
+++ b/vernac/declareDef.ml
@@ -36,7 +36,7 @@ let declare_global_definition ident ce local k pl imps =
   let kn = declare_constant ident ~local (DefinitionEntry ce, IsDefinition k) in
   let gr = ConstRef kn in
   let () = maybe_declare_manual_implicits false gr imps in
-  let () = Universes.register_universe_binders gr pl in
+  let () = Declare.declare_univ_binders gr pl in
   let () = definition_message ident in
   gr
 
@@ -49,6 +49,7 @@ let declare_definition ident (local, p, k) ce pl imps hook =
     let () = definition_message ident in
     let gr = VarRef ident in
     let () = maybe_declare_manual_implicits false gr imps in
+    let () = Declare.declare_univ_binders gr pl in
     let () = if Proof_global.there_are_pending_proofs () then
 	       warn_definition_not_visible ident
     in
diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index 42631a15b..200c2260e 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -177,7 +177,7 @@ let look_for_possibly_mutual_statements = function
 
 (* Saving a goal *)
 
-let save ?export_seff id const cstrs pl do_guard (locality,poly,kind) hook =
+let save ?export_seff id const uctx do_guard (locality,poly,kind) hook =
   let fix_exn = Future.fix_exn_of const.Entries.const_entry_body in
   try
     let const = adjust_guardness_conditions const do_guard in
@@ -204,7 +204,7 @@ let save ?export_seff id const cstrs pl do_guard (locality,poly,kind) hook =
           (locality, ConstRef kn)
     in
     definition_message id;
-    Universes.register_universe_binders r (Option.default Universes.empty_binders pl);
+    Declare.declare_univ_binders r (UState.universe_binders uctx);
     call_hook (fun exn -> exn) hook l r
   with e when CErrors.noncritical e ->
     let e = CErrors.push e in
@@ -286,17 +286,17 @@ let save_hook = ref ignore
 let set_save_hook f = save_hook := f
 
 let save_named ?export_seff proof =
-  let id,const,(cstrs,pl),do_guard,persistence,hook = proof in
-  save ?export_seff id const cstrs pl do_guard persistence hook
+  let id,const,uctx,do_guard,persistence,hook = proof in
+  save ?export_seff id const uctx do_guard persistence hook
 
 let check_anonymity id save_ident =
   if not (String.equal (atompart_of_id id) (Id.to_string (default_thm_id))) then
     user_err Pp.(str "This command can only be used for unnamed theorem.")
 
 let save_anonymous ?export_seff proof save_ident =
-  let id,const,(cstrs,pl),do_guard,persistence,hook = proof in
+  let id,const,uctx,do_guard,persistence,hook = proof in
   check_anonymity id save_ident;
-  save ?export_seff save_ident const cstrs pl do_guard persistence hook
+  save ?export_seff save_ident const uctx do_guard persistence hook
 
 (* Admitted *)
 
@@ -312,7 +312,7 @@ let admit (id,k,e) pl hook () =
   | Local, _, _ | Discharge, _, _ -> warn_let_as_axiom id
   in
   let () = assumption_message id in
-  Universes.register_universe_binders (ConstRef kn) (Option.default Universes.empty_binders pl);
+  Declare.declare_univ_binders (ConstRef kn) pl;
   call_hook (fun exn -> exn) hook Global (ConstRef kn)
 
 (* Starting a goal *)
@@ -330,8 +330,8 @@ let get_proof proof do_guard hook opacity =
 let universe_proof_terminator compute_guard hook =
   let open Proof_global in
   make_terminator begin function
-  | Admitted (id,k,pe,(ctx,pl)) ->
-      admit (id,k,pe) pl (hook (Some ctx)) ();
+  | Admitted (id,k,pe,ctx) ->
+      admit (id,k,pe) (UState.universe_binders ctx) (hook (Some ctx)) ();
       Feedback.feedback Feedback.AddedAxiom
   | Proved (opaque,idopt,proof) ->
       let is_opaque, export_seff = match opaque with
@@ -339,7 +339,7 @@ let universe_proof_terminator compute_guard hook =
         | Vernacexpr.Opaque      -> true, false
       in
       let proof = get_proof proof compute_guard
-	(hook (Some (fst proof.Proof_global.universes))) is_opaque in
+        (hook (Some (proof.Proof_global.universes))) is_opaque in
       begin match idopt with
       | None -> save_named ~export_seff proof
       | Some (_,id) -> save_anonymous ~export_seff proof id
@@ -417,7 +417,7 @@ let start_proof_with_initialization kind ctx decl recguard thms snl hook =
   | (id,(t,(_,imps)))::other_thms ->
       let hook ctx strength ref =
         let ctx = match ctx with
-        | None -> Evd.empty_evar_universe_context
+        | None -> UState.empty
         | Some ctx -> ctx
         in
         let other_thms_data =
@@ -426,9 +426,9 @@ let start_proof_with_initialization kind ctx decl recguard thms snl hook =
             let body,opaq = retrieve_first_recthm ctx ref in
             let subst = Evd.evar_universe_context_subst ctx in
             let norm c = Universes.subst_opt_univs_constr subst c in
-            let ctx = UState.check_univ_decl ~poly:(pi2 kind) ctx decl in
             let body = Option.map norm body in
-            List.map_i (save_remaining_recthms kind norm ctx body opaq) 1 other_thms in
+            let uctx = UState.check_univ_decl ~poly:(pi2 kind) ctx decl in
+            List.map_i (save_remaining_recthms kind norm uctx body opaq) 1 other_thms in
         let thms_data = (strength,ref,imps)::other_thms_data in
         List.iter (fun (strength,ref,imps) ->
 	  maybe_declare_manual_implicits false ref imps;
@@ -496,7 +496,7 @@ let save_proof ?proof = function
             if const_entry_type = None then
               user_err Pp.(str "Admitted requires an explicit statement");
             let typ = Option.get const_entry_type in
-            let ctx = UState.const_univ_entry ~poly:(pi2 k) (fst universes) in
+            let ctx = UState.const_univ_entry ~poly:(pi2 k) universes in
             let sec_vars = if !keep_admitted_vars then const_entry_secctx else None in
             Admitted(id, k, (sec_vars, (typ, ctx), None), universes)
         | None ->
@@ -518,12 +518,9 @@ let save_proof ?proof = function
                   Some (Environ.keep_hyps env (Id.Set.union ids_typ ids_def))
               | _ -> None in
 	    let decl = Proof_global.get_universe_decl () in
-            let evd = Evd.from_ctx universes in
             let poly = pi2 k in
-            let ctx = Evd.check_univ_decl ~poly evd decl in
-            let binders = if poly then Some (UState.universe_binders universes) else None in
-            Admitted(id,k,(sec_vars, (typ, ctx), None),
-		     (universes, binders))
+            let ctx = UState.check_univ_decl ~poly universes decl in
+            Admitted(id,k,(sec_vars, (typ, ctx), None), universes)
       in
       Proof_global.apply_terminator (Proof_global.get_terminator ()) pe
   | Vernacexpr.Proved (is_opaque,idopt) ->
diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index 1046d68f8..24d664951 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -833,7 +833,7 @@ let obligation_terminator name num guard hook auto pf =
     let entry = Safe_typing.inline_private_constants_in_definition_entry env entry in
     let ty = entry.Entries.const_entry_type in
     let (body, cstr), () = Future.force entry.Entries.const_entry_body in
-    let sigma = Evd.from_ctx (fst uctx) in
+    let sigma = Evd.from_ctx uctx in
     let sigma = Evd.merge_context_set ~sideff:true Evd.univ_rigid sigma cstr in
     Inductiveops.control_only_guard (Global.env ()) body;
     (** Declare the obligation ourselves and drop the hook *)
diff --git a/vernac/record.ml b/vernac/record.ml
index 1d255b08e..1cdc538b5 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -613,7 +613,7 @@ let definition_structure (kind,cum,poly,finite,(is_coe,((loc,idstruc),pl)),ps,cf
     States.with_state_protection (fun () ->
       typecheck_params_and_fields finite (kind = Class true) idstruc poly pl s ps notations fs) () in
   let sign = structure_signature (fields@params) in
-  match kind with
+  let gr = match kind with
   | Class def ->
      let priorities = List.map (fun id -> {hint_priority = id; hint_pattern = None}) priorities in
      let gr = declare_class finite def cum pl univs (loc,idstruc) idbuild
@@ -638,3 +638,6 @@ let definition_structure (kind,cum,poly,finite,(is_coe,((loc,idstruc),pl)),ps,cf
 	  idbuild implpars params arity template implfs 
 	  fields is_coe (List.map (fun coe -> not (Option.is_empty coe)) coers) sign in
 	IndRef ind
+  in
+  Declare.declare_univ_binders gr pl;
+  gr