Merge PR #1033: Universe binder improvements

12 files changed, 338 insertions, 318 deletions

diff --git a/vernac/class.ml b/vernac/class.ml
index 44f20a088..943da8fa8 100644
--- a/vernac/class.ml
+++ b/vernac/class.ml
@@ -212,10 +212,10 @@ let build_id_coercion idf_opt source poly =
 	  Id.of_string ("Id_"^(ident_key_of_class source)^"_"^
                         (ident_key_of_class cl))
   in
-  let univs = (snd (Evd.universe_context ~names:[] ~extensible:true sigma)) in
+  let univs = Evd.const_univ_entry ~poly sigma in
   let constr_entry = (* Cast is necessary to express [val_f] is identity *)
     DefinitionEntry
-      (definition_entry ~types:typ_f ~poly ~univs
+      (definition_entry ~types:typ_f ~univs
 	 ~inline:true (mkCast (val_f, DEFAULTcast, typ_f)))
   in
   let decl = (constr_entry, IsDefinition IdentityCoercion) in
diff --git a/vernac/classes.ml b/vernac/classes.ml
index 20cb43b24..b80741269 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -119,14 +119,14 @@ let declare_instance_constant k info global imps ?hook id decl poly evm term ter
 				 (Univops.universes_of_constr term) in
     Evd.restrict_universe_context evm levels 
   in
-  let pl, uctx = Evd.check_univ_decl evm decl in
+  let uctx = Evd.check_univ_decl ~poly evm decl in
   let entry = 
-    Declare.definition_entry ~types:termtype ~poly ~univs:uctx term
+    Declare.definition_entry ~types:termtype ~univs:uctx term
   in
   let cdecl = (DefinitionEntry entry, kind) in
   let kn = Declare.declare_constant id cdecl in
     Declare.definition_message id;
-    Universes.register_universe_binders (ConstRef kn) pl;
+    Universes.register_universe_binders (ConstRef kn) (Evd.universe_binders evm);
     instance_hook k info global imps ?hook (ConstRef kn);
     id
 
@@ -200,16 +200,16 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance)
 	let nf, subst = Evarutil.e_nf_evars_and_universes evars in
 	let termtype =
 	  let t = it_mkProd_or_LetIn ty_constr (ctx' @ ctx) in
-	    nf t
-	in
-	Pretyping.check_evars env Evd.empty !evars (EConstr.of_constr termtype);
-	let pl, ctx = Evd.check_univ_decl !evars decl in
-	let cst = Declare.declare_constant ~internal:Declare.InternalTacticRequest id
-	  (ParameterEntry 
-            (None,poly,(termtype,ctx),None), Decl_kinds.IsAssumption Decl_kinds.Logical)
-	in
-	  Universes.register_universe_binders (ConstRef cst) pl;
-	  instance_hook k pri global imps ?hook (ConstRef cst); id
+            nf t
+        in
+        Pretyping.check_evars env Evd.empty !evars (EConstr.of_constr termtype);
+        let univs = Evd.check_univ_decl ~poly !evars decl in
+        let cst = Declare.declare_constant ~internal:Declare.InternalTacticRequest id
+          (ParameterEntry
+            (None,(termtype,univs),None), Decl_kinds.IsAssumption Decl_kinds.Logical)
+        in
+          Universes.register_universe_binders (ConstRef cst) (Evd.universe_binders !evars);
+          instance_hook k pri global imps ?hook (ConstRef cst); id
       end
     else (
       let props =
@@ -384,14 +384,17 @@ let context poly l =
   let uctx = ref (Evd.universe_context_set !evars) in
   let fn status (id, b, t) =
     if Lib.is_modtype () && not (Lib.sections_are_opened ()) then
-      let ctx = Univ.ContextSet.to_context !uctx in
       (* Declare the universe context once *)
+      let univs = if poly
+        then Polymorphic_const_entry (Univ.ContextSet.to_context !uctx)
+        else Monomorphic_const_entry !uctx
+      in
       let () = uctx := Univ.ContextSet.empty in
       let decl = match b with
       | None ->
-        (ParameterEntry (None,poly,(t,ctx),None), IsAssumption Logical)
+        (ParameterEntry (None,(t,univs),None), IsAssumption Logical)
       | Some b ->
-        let entry = Declare.definition_entry ~poly ~univs:ctx ~types:t b in
+        let entry = Declare.definition_entry ~univs ~types:t b in
         (DefinitionEntry entry, IsAssumption Logical)
       in
       let cst = Declare.declare_constant ~internal:Declare.InternalTacticRequest id decl in
@@ -409,16 +412,19 @@ let context poly l =
       in
       let impl = List.exists test impls in
       let decl = (Discharge, poly, Definitional) in
+      let univs = if poly
+        then Polymorphic_const_entry (Univ.ContextSet.to_context !uctx)
+        else Monomorphic_const_entry !uctx
+      in
       let nstatus = match b with
       | None ->
-        pi3 (Command.declare_assumption false decl (t, !uctx) [] [] impl
+        pi3 (Command.declare_assumption false decl (t, univs) Universes.empty_binders [] impl
           Vernacexpr.NoInline (Loc.tag id))
       | Some b ->
-        let ctx = Univ.ContextSet.to_context !uctx in
         let decl = (Discharge, poly, Definition) in
-        let entry = Declare.definition_entry ~poly ~univs:ctx ~types:t b in
+        let entry = Declare.definition_entry ~univs ~types:t b in
         let hook = Lemmas.mk_hook (fun _ gr -> gr) in
-        let _ = DeclareDef.declare_definition id decl entry [] [] hook in
+        let _ = DeclareDef.declare_definition id decl entry Universes.empty_binders [] hook in
         Lib.sections_are_opened () || Lib.is_modtype_strict ()
       in
 	status && nstatus
diff --git a/vernac/command.ml b/vernac/command.ml
index 257c003b5..373e5a1be 100644
--- a/vernac/command.ml
+++ b/vernac/command.ml
@@ -88,7 +88,7 @@ let warn_implicits_in_term =
           strbrk "Implicit arguments declaration relies on type." ++ spc () ++
             strbrk "The term declares more implicits than the type here.")
         
-let interp_definition pl bl p red_option c ctypopt =
+let interp_definition pl bl poly red_option c ctypopt =
   let env = Global.env() in
   let evd, decl = Univdecls.interp_univ_decl_opt env pl in
   let evdref = ref evd in
@@ -105,14 +105,15 @@ let interp_definition pl bl p 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 pl, uctx = Evd.check_univ_decl evd decl in
- 	imps1@(Impargs.lift_implicits nb_args imps2), pl,
-	  definition_entry ~univs:uctx ~poly:p body
+        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,
+          definition_entry ~univs:uctx body
     | Some ctyp ->
-	let ty, impsty = interp_type_evars_impls ~impls env_bl evdref ctyp in
-	let subst = evd_comb0 Evd.nf_univ_variables evdref in
+        let ty, impsty = interp_type_evars_impls ~impls env_bl evdref ctyp in
+        let subst = evd_comb0 Evd.nf_univ_variables evdref in
 	let ctx = Context.Rel.map (Vars.subst_univs_constr subst) ctx in
 	let env_bl = push_rel_context ctx env in
 	let c, imps2 = interp_casted_constr_evars_impls ~impls env_bl evdref c ty in
@@ -133,9 +134,10 @@ let interp_definition pl bl p red_option c ctypopt =
         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 pl, uctx = Evd.check_univ_decl ctx decl in
-	imps1@(Impargs.lift_implicits nb_args impsty), pl,
-	  definition_entry ~types:typ ~poly:p 
+        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
   in
   red_constant_entry (Context.Rel.length ctx) ce !evdref red_option, !evdref, decl, pl, imps
@@ -175,6 +177,10 @@ let do_definition ident k univdecl bl red_option c ctypopt hook =
 let declare_assumption is_coe (local,p,kind) (c,ctx) pl imps impl nl (_,ident) =
 match local with
 | Discharge when Lib.sections_are_opened () ->
+  let ctx = match ctx with
+    | Monomorphic_const_entry ctx -> ctx
+    | Polymorphic_const_entry ctx -> Univ.ContextSet.of_context ctx
+  in
   let decl = (Lib.cwd(), SectionLocalAssum ((c,ctx),p,impl), IsAssumption kind) in
   let _ = declare_variable ident decl in
   let () = assumption_message ident in
@@ -195,8 +201,7 @@ match local with
     | DefaultInline -> Some (Flags.get_inline_level())
     | InlineAt i -> Some i
   in
-  let ctx = Univ.ContextSet.to_context ctx in
-  let decl = (ParameterEntry (None,p,(c,ctx),inl), IsAssumption kind) in
+  let decl = (ParameterEntry (None,(c,ctx),inl), IsAssumption kind) in
   let kn = declare_constant ident ~local decl in
   let gr = ConstRef kn in
   let () = maybe_declare_manual_implicits false gr imps in
@@ -204,9 +209,9 @@ match local with
   let () = assumption_message ident in
   let () = Typeclasses.declare_instance None false gr in
   let () = if is_coe then Class.try_add_new_coercion gr ~local p in
-  let inst = 
-    if p (* polymorphic *) then Univ.UContext.instance ctx 
-    else Univ.Instance.empty
+  let inst = match ctx with
+    | Polymorphic_const_entry ctx -> Univ.UContext.instance ctx
+    | Monomorphic_const_entry _ -> Univ.Instance.empty
   in
     (gr,inst,Lib.is_modtype_strict ())
 
@@ -216,26 +221,63 @@ let interp_assumption evdref env impls bl c =
   let ty = EConstr.Unsafe.to_constr ty in
   (ty, impls)
 
-let declare_assumptions idl is_coe k (c,ctx) pl imps impl_is_on nl =
+(* When monomorphic the universe constraints are declared with the first declaration only. *)
+let next_uctx =
+  let empty_uctx = Monomorphic_const_entry Univ.ContextSet.empty in
+  function
+  | Polymorphic_const_entry _ as uctx -> uctx
+  | Monomorphic_const_entry _ -> empty_uctx
+
+let declare_assumptions idl is_coe k (c,uctx) pl imps nl =
   let refs, status, _ =
-    List.fold_left (fun (refs,status,ctx) id ->
+    List.fold_left (fun (refs,status,uctx) id ->
       let ref',u',status' =
-	declare_assumption is_coe k (c,ctx) pl imps impl_is_on nl id in
-      (ref',u')::refs, status' && status, Univ.ContextSet.empty)
-      ([],true,ctx) idl
+        declare_assumption is_coe k (c,uctx) pl imps false nl id in
+      (ref',u')::refs, status' && status, next_uctx uctx)
+      ([],true,uctx) idl
   in
   List.rev refs, status
 
-let do_assumptions_unbound_univs (_, poly, _ as kind) nl l =
+
+let maybe_error_many_udecls = function
+  | ((loc,id), Some _) ->
+    user_err ?loc ~hdr:"many_universe_declarations"
+      Pp.(str "When declaring multiple axioms in one command, " ++
+          str "only the first is allowed a universe binder " ++
+          str "(which will be shared by the whole block).")
+  | (_, None) -> ()
+
+let process_assumptions_udecls kind l =
+  let udecl, first_id = match l with
+    | (coe, ((id, udecl)::rest, c))::rest' ->
+      List.iter maybe_error_many_udecls rest;
+      List.iter (fun (coe, (idl, c)) -> List.iter maybe_error_many_udecls idl) rest';
+      udecl, id
+    | (_, ([], _))::_ | [] -> assert false
+  in
+  let () = match kind, udecl with
+    | (Discharge, _, _), Some _ when Lib.sections_are_opened () ->
+      let loc = fst first_id in
+      let msg = Pp.str "Section variables cannot be polymorphic." in
+      user_err ?loc  msg
+    | _ -> ()
+  in
+  udecl, List.map (fun (coe, (idl, c)) -> coe, (List.map fst idl, c)) l
+
+let do_assumptions kind nl l =
   let open Context.Named.Declaration in
   let env = Global.env () in
-  let evdref = ref (Evd.from_env env) in
-  let l = 
-    if poly then
+  let udecl, l = process_assumptions_udecls kind l in
+  let evdref, udecl =
+    let evd, udecl = Univdecls.interp_univ_decl_opt env udecl in
+    ref evd, udecl
+  in
+  let l =
+    if pi2 kind (* poly *) then
       (* Separate declarations so that A B : Type puts A and B in different levels. *)
       List.fold_right (fun (is_coe,(idl,c)) acc ->
-        List.fold_right (fun id acc -> 
-	  (is_coe, ([id], c)) :: acc) idl acc)
+        List.fold_right (fun id acc ->
+          (is_coe, ([id], c)) :: acc) idl acc)
         l []
     else l
   in
@@ -247,65 +289,31 @@ let do_assumptions_unbound_univs (_, poly, _ as kind) nl l =
     let ienv = List.fold_right (fun (_,id) ienv ->
       let impls = compute_internalization_data env Variable t imps in
       Id.Map.add id impls ienv) idl ienv in
-      ((env,ienv),((is_coe,idl),t,imps))) 
+      ((env,ienv),((is_coe,idl),t,imps)))
     (env,empty_internalization_env) l
   in
   let evd = solve_remaining_evars all_and_fail_flags env !evdref Evd.empty in
   (* The universe constraints come from the whole telescope. *)
   let evd = Evd.nf_constraints evd in
-  let ctx = Evd.universe_context_set evd in
-  let nf_evar c = EConstr.Unsafe.to_constr (nf_evar evd (EConstr.of_constr c)) in
-  let l = List.map (on_pi2 nf_evar) l in
-  pi2 (List.fold_left (fun (subst,status,ctx) ((is_coe,idl),t,imps) ->
-    let t = replace_vars subst t in
-    let (refs,status') = declare_assumptions idl is_coe kind (t,ctx) [] imps false nl in
-    let subst' = List.map2 
-      (fun (_,id) (c,u) -> (id,Universes.constr_of_global_univ (c,u)))
-      idl refs 
-    in
-    (subst'@subst, status' && status,
-     (* The universe constraints are declared with the first declaration only. *)
-     Univ.ContextSet.empty)) ([],true,ctx) l)
-
-let do_assumptions_bound_univs coe kind nl id pl c =
-  let env = Global.env () in
-  let evd, decl = Univdecls.interp_univ_decl_opt env pl in
-  let evdref = ref evd in
-  let ty, impls = interp_type_evars_impls env evdref c in
-  let nf, subst = Evarutil.e_nf_evars_and_universes evdref in
-  let ty = EConstr.Unsafe.to_constr ty in
-  let ty = nf ty in
-  let vars = Univops.universes_of_constr ty in
-  let evd = Evd.restrict_universe_context !evdref vars in
-  let pl, uctx = Evd.check_univ_decl evd decl in
-  let uctx = Univ.ContextSet.of_context uctx in
-  let (_, _, st) = declare_assumption coe kind (ty, uctx) pl impls false nl id in
-  st
-
-let do_assumptions kind nl l = match l with
-| [coe, ([id, Some pl], c)] ->
-  let () = match kind with
-  | (Discharge, _, _) when Lib.sections_are_opened () ->
-    let loc = fst id in
-    let msg = Pp.str "Section variables cannot be polymorphic." in
-    user_err ?loc  msg
-  | _ -> ()
+  let nf_evar c = EConstr.to_constr evd (EConstr.of_constr c) in
+  let uvars, l = List.fold_left_map (fun uvars (coe,t,imps) ->
+      let t = nf_evar t in
+      let uvars = Univ.LSet.union uvars (Univops.universes_of_constr t) in
+      uvars, (coe,t,imps))
+      Univ.LSet.empty l
   in
-  do_assumptions_bound_univs coe kind nl id (Some pl) c
-| _ ->
-  let map (coe, (idl, c)) =
-    let map (id, univs) = match univs with
-    | None -> id
-    | Some _ ->
-      let loc = fst id in
-      let msg =
-	Pp.str "Assumptions with bound universes can only be defined one at a time." in
-      user_err ?loc  msg
-    in
-    (coe, (List.map map idl, c))
-  in
-  let l = List.map map l in
-  do_assumptions_unbound_univs kind nl l
+  let evd = Evd.restrict_universe_context evd uvars in
+  let uctx = Evd.check_univ_decl ~poly:(pi2 kind) evd udecl in
+  let ubinders = Evd.universe_binders evd in
+  pi2 (List.fold_left (fun (subst,status,uctx) ((is_coe,idl),t,imps) ->
+      let t = replace_vars subst t in
+      let refs, status' = declare_assumptions idl is_coe kind (t,uctx) ubinders imps nl in
+      let subst' = List.map2
+          (fun (_,id) (c,u) -> (id, Universes.constr_of_global_univ (c,u)))
+          idl refs
+      in
+      subst'@subst, status' && status, next_uctx uctx)
+    ([], true, uctx) l)
 
 (* 3a| Elimination schemes for mutual inductive definitions *)
 
@@ -576,7 +584,7 @@ let interp_mutual_inductive (paramsl,indl) notations cum poly prv finite =
   let constructors = List.map (fun (idl,cl,impsl) -> (idl,List.map nf' cl,impsl)) constructors in
   let ctx_params = Context.Rel.map nf ctx_params in
   let evd = !evdref in
-  let pl, uctx = Evd.check_univ_decl evd decl in
+  let uctx = Evd.check_univ_decl ~poly evd decl in
   List.iter (fun c -> check_evars env_params Evd.empty evd (EConstr.of_constr c)) arities;
   Context.Rel.iter (fun c -> check_evars env0 Evd.empty evd (EConstr.of_constr c)) ctx_params;
   List.iter (fun (_,ctyps,_) ->
@@ -598,11 +606,12 @@ let interp_mutual_inductive (paramsl,indl) notations cum poly prv finite =
 	  userimpls @ (lift_implicits len impls)) cimpls) indimpls constructors
   in
   let univs =
-    if poly then
+    match uctx with
+    | Polymorphic_const_entry uctx ->
       if cum then
         Cumulative_ind_entry (Universes.univ_inf_ind_from_universe_context uctx)
       else Polymorphic_ind_entry uctx
-    else
+    | Monomorphic_const_entry uctx ->
       Monomorphic_ind_entry uctx
   in
   (* Build the mutual inductive entry *)
@@ -617,7 +626,7 @@ let interp_mutual_inductive (paramsl,indl) notations cum poly prv finite =
   in
   (if poly && cum then
       Inductiveops.infer_inductive_subtyping env_ar evd mind_ent
-   else mind_ent), pl, impls
+   else mind_ent), Evd.universe_binders evd, impls
 
 (* Very syntactical equality *)
 let eq_local_binders bl1 bl2 =
@@ -1019,23 +1028,22 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation =
   let binders_rel = nf_evar_context !evdref binders_rel in
   let binders = nf_evar_context !evdref binders in
   let top_arity = Evarutil.nf_evar !evdref top_arity in
-  let pl, plext = Option.cata
-      (fun d -> d.univdecl_instance, d.univdecl_extensible_instance) ([],true) pl in
   let hook, recname, typ =
     if List.length binders_rel > 1 then
       let name = add_suffix recname "_func" in
       let hook l gr _ = 
-	let body = it_mkLambda_or_LetIn (mkApp (Evarutil.e_new_global evdref gr, [|make|])) binders_rel in
-	let ty = it_mkProd_or_LetIn top_arity binders_rel in
-	let ty = EConstr.Unsafe.to_constr ty in
-	let pl, univs = Evd.universe_context ~names:pl ~extensible:plext !evdref in
-	  (*FIXME poly? *)
-	let ce = definition_entry ~poly ~types:ty ~univs (EConstr.to_constr !evdref body) in
-	(** FIXME: include locality *)
-	let c = Declare.declare_constant recname (DefinitionEntry ce, IsDefinition Definition) in
-	let gr = ConstRef c in
-	  if Impargs.is_implicit_args () || not (List.is_empty impls) then
-	    Impargs.declare_manual_implicits false gr [impls]
+        let body = it_mkLambda_or_LetIn (mkApp (Evarutil.e_new_global evdref gr, [|make|])) binders_rel in
+        let ty = it_mkProd_or_LetIn top_arity binders_rel in
+        let ty = EConstr.Unsafe.to_constr ty in
+        let univs = Evd.check_univ_decl ~poly !evdref decl in
+        (*FIXME poly? *)
+        let ce = definition_entry ~types:ty ~univs (EConstr.to_constr !evdref body) in
+        (** FIXME: include locality *)
+        let c = Declare.declare_constant recname (DefinitionEntry ce, IsDefinition Definition) in
+        let gr = ConstRef c in
+        let () = Universes.register_universe_binders gr (Evd.universe_binders !evdref) in
+        if Impargs.is_implicit_args () || not (List.is_empty impls) then
+          Impargs.declare_manual_implicits false gr [impls]
       in
       let typ = it_mkProd_or_LetIn top_arity binders in
 	hook, name, typ
@@ -1168,7 +1176,8 @@ let declare_fixpoint local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) ind
       List.map_i (fun i _ -> mkFix ((indexes,i),fixdecls)) 0 fixnames in
     let evd = Evd.from_ctx ctx in
     let evd = Evd.restrict_universe_context evd vars in
-    let pl, ctx = Evd.check_univ_decl evd pl in
+    let ctx = Evd.check_univ_decl ~poly evd pl in
+    let pl = Evd.universe_binders evd in
     let fixdecls = List.map Safe_typing.mk_pure_proof fixdecls in
     ignore (List.map4 (DeclareDef.declare_fix (local, poly, Fixpoint) pl ctx)
 	      fixnames fixdecls fixtypes fiximps);
@@ -1200,7 +1209,8 @@ let declare_cofixpoint local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) n
     let fiximps = List.map (fun (len,imps,idx) -> imps) fiximps in
     let evd = Evd.from_ctx ctx in
     let evd = Evd.restrict_universe_context evd vars in
-    let pl, ctx = Evd.check_univ_decl evd pl in
+    let ctx = Evd.check_univ_decl ~poly evd pl in
+    let pl = Evd.universe_binders evd in
     ignore (List.map4 (DeclareDef.declare_fix (local, poly, CoFixpoint) pl ctx)
 	      fixnames fixdecls fixtypes fiximps);
     (* Declare the recursive definitions *)
diff --git a/vernac/command.mli b/vernac/command.mli
index fb99a717b..070f3e112 100644
--- a/vernac/command.mli
+++ b/vernac/command.mli
@@ -43,7 +43,7 @@ val do_definition : Id.t -> definition_kind -> Vernacexpr.universe_decl_expr opt
 (** returns [false] if the assumption is neither local to a section,
     nor in a module type and meant to be instantiated. *)
 val declare_assumption : coercion_flag -> assumption_kind -> 
-  types Univ.in_universe_context_set ->
+  types in_constant_universes_entry ->
   Universes.universe_binders -> Impargs.manual_implicits ->
   bool (** implicit *) -> Vernacexpr.inline -> variable Loc.located ->
   global_reference * Univ.Instance.t * bool
diff --git a/vernac/declareDef.ml b/vernac/declareDef.ml
index c18744052..980db4109 100644
--- a/vernac/declareDef.ml
+++ b/vernac/declareDef.ml
@@ -57,7 +57,7 @@ let declare_definition ident (local, p, k) ce pl imps hook =
     declare_global_definition ident ce local k pl imps in
   Lemmas.call_hook fix_exn hook local r
 
-let declare_fix ?(opaque = false) (_,poly,_ as kind) pl ctx f ((def,_),eff) t imps =
-  let ce = definition_entry ~opaque ~types:t ~poly ~univs:ctx ~eff def in
+let declare_fix ?(opaque = false) (_,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 (Lemmas.mk_hook (fun _ r -> r))
 
diff --git a/vernac/declareDef.mli b/vernac/declareDef.mli
index 01a87818a..55f7c7861 100644
--- a/vernac/declareDef.mli
+++ b/vernac/declareDef.mli
@@ -15,5 +15,8 @@ val declare_definition : Id.t -> definition_kind ->
   Safe_typing.private_constants Entries.definition_entry -> Universes.universe_binders -> Impargs.manual_implicits ->
     Globnames.global_reference Lemmas.declaration_hook -> Globnames.global_reference
 
-val declare_fix : ?opaque:bool -> definition_kind -> Universes.universe_binders -> Univ.UContext.t -> Id.t ->
-  Safe_typing.private_constants Entries.proof_output -> Constr.types -> Impargs.manual_implicits -> Globnames.global_reference
+val declare_fix : ?opaque:bool -> definition_kind ->
+  Universes.universe_binders -> Entries.constant_universes_entry ->
+  Id.t -> Safe_typing.private_constants Entries.proof_output ->
+  Constr.types -> Impargs.manual_implicits ->
+  Globnames.global_reference
diff --git a/vernac/indschemes.ml b/vernac/indschemes.ml
index c0ddc7e2c..e4ca98749 100644
--- a/vernac/indschemes.ml
+++ b/vernac/indschemes.ml
@@ -109,10 +109,10 @@ let _ =
 
 let define id internal ctx c t =
   let f = declare_constant ~internal in
-  let _, univs = Evd.universe_context ~names:[] ~extensible:true ctx in
   let univs =
-    if Flags.is_universe_polymorphism () then Polymorphic_const_entry univs
-    else Monomorphic_const_entry univs
+    if Flags.is_universe_polymorphism ()
+    then Polymorphic_const_entry (Evd.to_universe_context ctx)
+    else Monomorphic_const_entry (Evd.universe_context_set ctx)
   in
   let kn = f id
     (DefinitionEntry
diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index a025bfff8..42631a15b 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -49,7 +49,8 @@ let retrieve_first_recthm uctx = function
       (NamedDecl.get_value (Global.lookup_named id),variable_opacity id)
   | ConstRef cst ->
       let cb = Global.lookup_constant cst in
-      let (_, uctx) = UState.universe_context ~names:[] ~extensible:true uctx in
+      (* we get the right order somehow but surely it could be enforced in a better way *)
+      let uctx = UState.context uctx in
       let inst = Univ.UContext.instance uctx in
       let map (c, ctx) = Vars.subst_instance_constr inst c in
       (Option.map map (Global.body_of_constant_body cb), is_opaque cb)
@@ -203,7 +204,7 @@ let save ?export_seff id const cstrs pl do_guard (locality,poly,kind) hook =
           (locality, ConstRef kn)
     in
     definition_message id;
-    Option.iter (Universes.register_universe_binders r) pl;
+    Universes.register_universe_binders r (Option.default Universes.empty_binders pl);
     call_hook (fun exn -> exn) hook l r
   with e when CErrors.noncritical e ->
     let e = CErrors.push e in
@@ -223,7 +224,7 @@ let compute_proof_name locality = function
     let avoid = Id.Set.of_list (Proof_global.get_all_proof_names ()) in
       next_global_ident_away default_thm_id avoid
 
-let save_remaining_recthms (locality,p,kind) norm ctx binders body opaq i (id,(t_i,(_,imps))) =
+let save_remaining_recthms (locality,p,kind) norm univs body opaq i (id,(t_i,(_,imps))) =
   let t_i = norm t_i in
   match body with
   | None ->
@@ -231,7 +232,13 @@ let save_remaining_recthms (locality,p,kind) norm ctx binders body opaq i (id,(t
       | Discharge ->
           let impl = false in (* copy values from Vernacentries *)
           let k = IsAssumption Conjectural in
-          let c = SectionLocalAssum ((t_i,Univ.ContextSet.of_context ctx),p,impl) in
+          let univs = match univs with
+            | Polymorphic_const_entry univs ->
+              (* What is going on here? *)
+              Univ.ContextSet.of_context univs
+            | Monomorphic_const_entry univs -> univs
+          in
+          let c = SectionLocalAssum ((t_i, univs),p,impl) in
 	  let _ = declare_variable id (Lib.cwd(),c,k) in
           (Discharge, VarRef id,imps)
       | Local | Global ->
@@ -241,7 +248,7 @@ let save_remaining_recthms (locality,p,kind) norm ctx binders body opaq i (id,(t
           | Global -> false
           | Discharge -> assert false
           in
-          let decl = (ParameterEntry (None,p,(t_i,ctx),None), k) in
+          let decl = (ParameterEntry (None,(t_i,univs),None), k) in
           let kn = declare_constant id ~local decl in
           (locality,ConstRef kn,imps))
   | Some body ->
@@ -259,8 +266,7 @@ let save_remaining_recthms (locality,p,kind) norm ctx binders body opaq i (id,(t
       let body_i = body_i body in
       match locality with
       | Discharge ->
-          let const = definition_entry ~types:t_i ~opaque:opaq ~poly:p 
-	    ~univs:ctx body_i in
+          let const = definition_entry ~types:t_i ~opaque:opaq ~univs body_i in
 	  let c = SectionLocalDef const in
 	  let _ = declare_variable id (Lib.cwd(), c, k) in
           (Discharge,VarRef id,imps)
@@ -271,7 +277,7 @@ let save_remaining_recthms (locality,p,kind) norm ctx binders body opaq i (id,(t
         | Discharge -> assert false
         in
         let const =
-	  Declare.definition_entry ~types:t_i ~poly:p ~univs:ctx ~opaque:opaq body_i
+          Declare.definition_entry ~types:t_i ~univs ~opaque:opaq body_i
 	in
         let kn = declare_constant id ~local (DefinitionEntry const, k) in
         (locality,ConstRef kn,imps)
@@ -306,7 +312,7 @@ let admit (id,k,e) pl hook () =
   | Local, _, _ | Discharge, _, _ -> warn_let_as_axiom id
   in
   let () = assumption_message id in
-  Option.iter (Universes.register_universe_binders (ConstRef kn)) pl;
+  Universes.register_universe_binders (ConstRef kn) (Option.default Universes.empty_binders pl);
   call_hook (fun exn -> exn) hook Global (ConstRef kn)
 
 (* Starting a goal *)
@@ -420,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 binders, ctx = Evd.check_univ_decl (Evd.from_ctx ctx) decl in
-	    let body = Option.map norm body in
-            List.map_i (save_remaining_recthms kind norm ctx binders body opaq) 1 other_thms 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 thms_data = (strength,ref,imps)::other_thms_data in
         List.iter (fun (strength,ref,imps) ->
 	  maybe_declare_manual_implicits false ref imps;
@@ -453,9 +459,9 @@ let start_proof_com ?inference_hook kind thms hook =
   let evd, nf = Evarutil.nf_evars_and_universes !evdref in
   let thms = List.map (fun (n, (t, info)) -> (n, (nf t, info))) thms in
   let () =
-    if not decl.Misctypes.univdecl_extensible_instance then
-       ignore (Evd.universe_context evd ~names:decl.Misctypes.univdecl_instance ~extensible:false)
-    else ()
+    let open Misctypes in
+    if not (decl.univdecl_extensible_instance && decl.univdecl_extensible_constraints) then
+       ignore (Evd.check_univ_decl ~poly:(pi2 kind) evd decl)
   in
   let evd =
     if pi2 kind then evd
@@ -490,9 +496,9 @@ 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 = Evd.evar_context_universe_context (fst universes) in
+            let ctx = UState.const_univ_entry ~poly:(pi2 k) (fst universes) in
             let sec_vars = if !keep_admitted_vars then const_entry_secctx else None in
-            Admitted(id, k, (sec_vars, pi2 k, (typ, ctx), None), universes)
+            Admitted(id, k, (sec_vars, (typ, ctx), None), universes)
         | None ->
             let pftree = Proof_global.give_me_the_proof () in
             let id, k, typ = Pfedit.current_proof_statement () in
@@ -513,10 +519,10 @@ let save_proof ?proof = function
               | _ -> None in
 	    let decl = Proof_global.get_universe_decl () in
             let evd = Evd.from_ctx universes in
-            let binders, ctx = Evd.check_univ_decl evd decl in
             let poly = pi2 k in
-            let binders = if poly then Some binders else None in
-            Admitted(id,k,(sec_vars, poly, (typ, ctx), None),
+            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))
       in
       Proof_global.apply_terminator (Proof_global.get_terminator ()) pe
diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index 700fd6045..1046d68f8 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -475,20 +475,17 @@ let declare_definition prg =
     (Evd.evar_universe_context_subst prg.prg_ctx) in
   let opaque = prg.prg_opaque in
   let fix_exn = Hook.get get_fix_exn () in
-  let pl, ctx = Evd.check_univ_decl (Evd.from_ctx prg.prg_ctx) prg.prg_univdecl in
-  let ce =
-    definition_entry ~fix_exn
-     ~opaque ~types:(nf typ) ~poly:(pi2 prg.prg_kind)
-     ~univs:(Evd.evar_context_universe_context prg.prg_ctx) (nf body)
-  in
+  let typ = nf typ in
+  let body = nf body in
+  let uvars = Univ.LSet.union (Univops.universes_of_constr typ) (Univops.universes_of_constr body) in
+  let uctx = UState.restrict prg.prg_ctx uvars in
+  let univs = UState.check_univ_decl ~poly:(pi2 prg.prg_kind) uctx prg.prg_univdecl in
+  let ce = definition_entry ~fix_exn ~opaque ~types:typ ~univs body in
   let () = progmap_remove prg in
-  let cst =
-    DeclareDef.declare_definition 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 prg.prg_ctx; r))
-  in
-  Universes.register_universe_binders cst pl;
-  cst
+  let ubinders = UState.universe_binders uctx in
+  DeclareDef.declare_definition prg.prg_name
+    prg.prg_kind ce ubinders prg.prg_implicits
+    (Lemmas.mk_hook (fun l r -> Lemmas.call_hook fix_exn prg.prg_hook l r uctx; r))
 
 let rec lam_index n t acc =
   match Constr.kind t with
@@ -552,9 +549,9 @@ let declare_mutual_definition l =
             mk_proof (mkCoFix (i,fixdecls))) 0 l
   in
   (* Declare the recursive definitions *)
-  let ctx = Evd.evar_context_universe_context first.prg_ctx in
+  let univs = UState.const_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) [] ctx)
+  let kns = List.map4 (DeclareDef.declare_fix ~opaque (local, poly, kind) Universes.empty_binders univs)
     fixnames fixdecls fixtypes fiximps in
     (* Declare notations *)
     List.iter (Metasyntax.add_notation_interpretation (Global.env())) first.prg_notations;
@@ -636,12 +633,11 @@ let declare_obligation prg obl body ty uctx =
 	  shrink_body body ty else [], body, ty, [||]
       in
       let body = ((body,Univ.ContextSet.empty),Safe_typing.empty_private_constants) in
-      let univs = if poly then Polymorphic_const_entry uctx else Monomorphic_const_entry uctx in
       let ce =
         { const_entry_body = Future.from_val ~fix_exn:(fun x -> x) body;
           const_entry_secctx = None;
 	  const_entry_type = ty;
-	  const_entry_universes = univs;
+          const_entry_universes = uctx;
 	  const_entry_opaque = opaque;
           const_entry_inline_code = false;
           const_entry_feedback = None;
@@ -650,13 +646,15 @@ let declare_obligation prg obl body ty uctx =
       let constant = Declare.declare_constant obl.obl_name ~local:true
 	(DefinitionEntry ce,IsProof Property)
       in
-	if not opaque then add_hint (Locality.make_section_locality None) prg constant;
-	definition_message obl.obl_name;
-	true, { obl with obl_body =
-	    if poly then
-	      Some (DefinedObl (constant, Univ.UContext.instance uctx))
-	    else
-	      Some (TermObl (it_mkLambda_or_LetIn_or_clean (mkApp (mkConst constant, args)) ctx)) }
+      if not opaque then add_hint (Locality.make_section_locality None) prg constant;
+      definition_message obl.obl_name;
+      let body = match uctx with
+        | Polymorphic_const_entry uctx ->
+          Some (DefinedObl (constant, Univ.UContext.instance uctx))
+        | Monomorphic_const_entry _ ->
+          Some (TermObl (it_mkLambda_or_LetIn_or_clean (mkApp (mkConst constant, args)) ctx))
+      in
+      true, { obl with obl_body = body }
 
 let init_prog_info ?(opaque = false) sign n udecl b t ctx deps fixkind
 		   notations obls impls kind reduce hook =
@@ -830,49 +828,63 @@ let obligation_terminator name num guard hook auto pf =
   match pf with
   | Admitted _ -> apply_terminator term pf
   | Proved (opq, id, proof) ->
-    if not !shrink_obligations then apply_terminator term pf
-    else
-      let (_, (entry, uctx, _)) = Pfedit.cook_this_proof proof in
-      let env = Global.env () in
-      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.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 *)
-      let prg = get_info (ProgMap.find name !from_prg) in
-      (** Ensure universes are substituted properly in body and type *)
-      let body = EConstr.to_constr sigma (EConstr.of_constr body) in
-      let ty = Option.map (fun x -> EConstr.to_constr sigma (EConstr.of_constr x)) ty in
-      let ctx = Evd.evar_universe_context sigma in
-      let prg = { prg with prg_ctx = ctx } in
-      let obls, rem = prg.prg_obligations in
-      let obl = obls.(num) in
-      let status =
-        match obl.obl_status, opq with
-        | (_, Evar_kinds.Expand), Vernacexpr.Opaque -> err_not_transp ()
-        | (true, _), Vernacexpr.Opaque -> err_not_transp ()
-        | (false, _), Vernacexpr.Opaque -> Evar_kinds.Define true
-        | (_, Evar_kinds.Define true), Vernacexpr.Transparent -> Evar_kinds.Define false
-        | (_, status), Vernacexpr.Transparent -> status
-      in
-      let obl = { obl with obl_status = false, status } in
-      let uctx = Evd.evar_context_universe_context ctx in
-      let (_, obl) = declare_obligation prg obl body ty uctx in
-      let obls = Array.copy obls in
-      let _ = obls.(num) <- obl in
-      try
+    let (_, (entry, uctx, _)) = Pfedit.cook_this_proof proof in
+    let env = Global.env () in
+    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.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 *)
+    let prg = get_info (ProgMap.find name !from_prg) in
+    (** Ensure universes are substituted properly in body and type *)
+    let body = EConstr.to_constr sigma (EConstr.of_constr body) in
+    let ty = Option.map (fun x -> EConstr.to_constr sigma (EConstr.of_constr x)) ty in
+    let ctx = Evd.evar_universe_context sigma in
+    let obls, rem = prg.prg_obligations in
+    let obl = obls.(num) in
+    let status =
+      match obl.obl_status, opq with
+      | (_, Evar_kinds.Expand), Vernacexpr.Opaque -> err_not_transp ()
+      | (true, _), Vernacexpr.Opaque -> err_not_transp ()
+      | (false, _), Vernacexpr.Opaque -> Evar_kinds.Define true
+      | (_, Evar_kinds.Define true), Vernacexpr.Transparent ->
+        Evar_kinds.Define false
+      | (_, status), Vernacexpr.Transparent -> status
+    in
+    let obl = { obl with obl_status = false, status } in
+    let ctx =
+      if pi2 prg.prg_kind then ctx
+      else UState.union prg.prg_ctx ctx
+    in
+    let uctx = UState.const_univ_entry ~poly:(pi2 prg.prg_kind) ctx in
+    let (_, obl) = declare_obligation prg obl body ty uctx in
+    let obls = Array.copy obls in
+    let _ = obls.(num) <- obl in
+    let prg_ctx =
+      if pi2 (prg.prg_kind) then (* Polymorphic *)
+        (** We merge the new universes and constraints of the
+            polymorphic obligation with the existing ones *)
+        UState.union prg.prg_ctx ctx
+      else
+        (** The first obligation declares the univs of the constant,
+            each subsequent obligation declares its own additional
+            universes and constraints if any *)
+        UState.make (Global.universes ())
+    in
+    let prg = { prg with prg_ctx } in
+    try
       ignore (update_obls prg obls (pred rem));
       if pred rem > 0 then
         begin
-	  let deps = dependencies obls num in
-	  if not (Int.Set.is_empty deps) then
-	    ignore (auto (Some name) None deps)
-	end
-      with e when CErrors.noncritical e ->
-        let e = CErrors.push e in
-        pperror (CErrors.iprint (ExplainErr.process_vernac_interp_error e))
+          let deps = dependencies obls num in
+          if not (Int.Set.is_empty deps) then
+            ignore (auto (Some name) None deps)
+        end
+    with e when CErrors.noncritical e ->
+      let e = CErrors.push e in
+      pperror (CErrors.iprint (ExplainErr.process_vernac_interp_error e))
 
 let obligation_hook prg obl num auto ctx' _ gr =
   let obls, rem = prg.prg_obligations in
@@ -893,7 +905,8 @@ in
       let ctx' = Evd.merge_universe_subst evd (Evd.universe_subst (Evd.from_ctx ctx')) in
       Univ.Instance.empty, Evd.evar_universe_context ctx'
     else
-      let (_, uctx) = UState.universe_context ~names:[] ~extensible:true ctx' in
+      (* We get the right order somehow, but surely it could be enforced in a clearer way. *)
+      let uctx = UState.context ctx' in
       Univ.UContext.instance uctx, ctx'
   in
   let obl = { obl with obl_body = Some (DefinedObl (cst, inst)) } in
@@ -969,13 +982,16 @@ and solve_obligation_by_tac prg obls i tac =
 	    let evd = Evd.from_ctx prg.prg_ctx in
 	    let evd = Evd.update_sigma_env evd (Global.env ()) in
 	    let t, ty, ctx =
-	      solve_by_tac obl.obl_name (evar_of_obligation obl) tac
-	        (pi2 prg.prg_kind) (Evd.evar_universe_context evd)
-	    in
-	    let uctx = Evd.evar_context_universe_context ctx in
-	    let prg = {prg with prg_ctx = ctx} in
-	    let def, obl' = declare_obligation prg obl t ty uctx in
-	      obls.(i) <- obl';
+              solve_by_tac obl.obl_name (evar_of_obligation obl) tac
+                (pi2 prg.prg_kind) (Evd.evar_universe_context evd)
+            in
+            let uctx = if pi2 prg.prg_kind
+              then Polymorphic_const_entry (UState.context ctx)
+              else Monomorphic_const_entry (UState.context_set ctx)
+            in
+            let prg = {prg with prg_ctx = ctx} in
+            let def, obl' = declare_obligation prg obl t ty uctx in
+              obls.(i) <- obl';
 	      if def && not (pi2 prg.prg_kind) then (
 	        (* Declare the term constraints with the first obligation only *)
 	        let evd = Evd.from_env (Global.env ()) in
@@ -1123,9 +1139,9 @@ let admit_prog prg =
         match x.obl_body with
         | None ->
             let x = subst_deps_obl obls x in
-	    let ctx = Evd.evar_context_universe_context prg.prg_ctx in
+            let ctx = Monomorphic_const_entry (UState.context_set prg.prg_ctx) in
             let kn = Declare.declare_constant x.obl_name ~local:true
-              (ParameterEntry (None,false,(x.obl_type,ctx),None), IsAssumption Conjectural)
+              (ParameterEntry (None,(x.obl_type,ctx),None), IsAssumption Conjectural)
             in
               assumption_message x.obl_name;
               obls.(i) <- { x with obl_body = Some (DefinedObl (kn, Univ.Instance.empty)) }
diff --git a/vernac/record.ml b/vernac/record.ml
index f09b57048..1d255b08e 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -95,7 +95,7 @@ let binder_of_decl = function
 
 let binders_of_decls = List.map binder_of_decl
 
-let typecheck_params_and_fields finite def id pl t ps nots fs =
+let typecheck_params_and_fields finite def id poly pl t ps nots fs =
   let env0 = Global.env () in
   let evd, decl = Univdecls.interp_univ_decl_opt env0 pl in
   let evars = ref evd in
@@ -167,10 +167,11 @@ let typecheck_params_and_fields finite def id pl t ps nots fs =
   let newps = List.map (EConstr.to_rel_decl evars) newps in
   let typ = EConstr.to_constr evars typ in
   let ce t = Pretyping.check_evars env0 Evd.empty evars (EConstr.of_constr t) in
-  let univs = Evd.check_univ_decl evars decl in
+  let univs = Evd.check_univ_decl ~poly evars decl in
+  let ubinders = Evd.universe_binders evars in
     List.iter (iter_constr ce) (List.rev newps);
     List.iter (iter_constr ce) (List.rev newfs);
-    univs, typ, template, imps, newps, impls, newfs
+    ubinders, univs, typ, template, imps, newps, impls, newfs
 
 let degenerate_decl decl =
   let id = match RelDecl.get_name decl with
@@ -265,12 +266,14 @@ let warn_non_primitive_record =
                     strbrk" could not be defined as a primitive record")))
 
 (* We build projections *)
-let declare_projections indsp ?(kind=StructureComponent) binder_name coers fieldimpls fields =
+let declare_projections indsp ctx ?(kind=StructureComponent) binder_name coers ubinders fieldimpls fields =
   let env = Global.env() in
   let (mib,mip) = Global.lookup_inductive indsp in
   let poly = Declareops.inductive_is_polymorphic mib in
-  let ctx = Univ.AUContext.repr (Declareops.inductive_polymorphic_context mib) in
-  let u = Univ.UContext.instance ctx in
+  let u = match ctx with
+    | Polymorphic_const_entry ctx -> Univ.UContext.instance ctx
+    | Monomorphic_const_entry ctx -> Univ.Instance.empty
+  in
   let paramdecls = Inductive.inductive_paramdecls (mib, u) in
   let indu = indsp, u in
   let r = mkIndU (indsp,u) in
@@ -304,9 +307,11 @@ let declare_projections indsp ?(kind=StructureComponent) binder_name coers field
 	    let kn, term = 
 	      if is_local_assum decl && primitive then
 		(** Already defined in the kernel silently *)
-		let kn = destConstRef (Nametab.locate (Libnames.qualid_of_ident fid)) in
-		  Declare.definition_message fid;
-		  kn, mkProj (Projection.make kn false,mkRel 1)
+                let gr = Nametab.locate (Libnames.qualid_of_ident fid) in
+                let kn = destConstRef gr in
+                Declare.definition_message fid;
+                Universes.register_universe_binders gr ubinders;
+                kn, mkProj (Projection.make kn false,mkRel 1)
 	      else
 		let ccl = subst_projection fid subst ti in
 		let body = match decl with
@@ -325,16 +330,12 @@ let declare_projections indsp ?(kind=StructureComponent) binder_name coers field
 		let projtyp =
                   it_mkProd_or_LetIn (mkProd (x,rp,ccl)) paramdecls in
 	        try
-                  let univs =
-                    if poly then Polymorphic_const_entry ctx
-                    else Monomorphic_const_entry ctx
-                  in
 		  let entry = {
 		    const_entry_body =
 		      Future.from_val (Safe_typing.mk_pure_proof proj);
 		    const_entry_secctx = None;
 		    const_entry_type = Some projtyp;
-		    const_entry_universes = univs;
+                    const_entry_universes = ctx;
 		    const_entry_opaque = false;
 		    const_entry_inline_code = false;
 		    const_entry_feedback = None } in
@@ -343,8 +344,9 @@ let declare_projections indsp ?(kind=StructureComponent) binder_name coers field
 		  let constr_fip =
 		    let proj_args = (*Rel 1 refers to "x"*) paramargs@[mkRel 1] in
 		      applist (mkConstU (kn,u),proj_args) 
-		  in
-		    Declare.definition_message fid;
+                  in
+                  Declare.definition_message fid;
+                  Universes.register_universe_binders (ConstRef kn) ubinders;
 		    kn, constr_fip
                 with Type_errors.TypeError (ctx,te) ->
                   raise (NotDefinable (BadTypedProj (fid,ctx,te))) 
@@ -382,17 +384,20 @@ let structure_signature ctx =
 
 open Typeclasses
 
-let declare_structure finite univs id idbuild paramimpls params arity template 
+let declare_structure finite ubinders univs id idbuild paramimpls params arity template
     fieldimpls fields ?(kind=StructureComponent) ?name is_coe coers sign =
   let nparams = List.length params and nfields = List.length fields in
   let args = Context.Rel.to_extended_list mkRel nfields params in
   let ind = applist (mkRel (1+nparams+nfields), args) in
   let type_constructor = it_mkProd_or_LetIn ind fields in
-  let poly, ctx =
+  let template, ctx =
     match univs with
-    | Monomorphic_ind_entry ctx -> false, ctx
-    | Polymorphic_ind_entry ctx -> true, ctx
-    | Cumulative_ind_entry cumi -> true, (Univ.CumulativityInfo.univ_context cumi)
+    | Monomorphic_ind_entry ctx ->
+      template, Monomorphic_const_entry Univ.ContextSet.empty
+    | Polymorphic_ind_entry ctx ->
+      false, Polymorphic_const_entry ctx
+    | Cumulative_ind_entry cumi ->
+      false, Polymorphic_const_entry (Univ.CumulativityInfo.univ_context cumi)
   in
   let binder_name = 
     match name with
@@ -402,7 +407,7 @@ let declare_structure finite univs id idbuild paramimpls params arity template
   let mie_ind =
     { mind_entry_typename = id;
       mind_entry_arity = arity;
-      mind_entry_template = not poly && template;
+      mind_entry_template = template;
       mind_entry_consnames = [idbuild];
       mind_entry_lc = [type_constructor] }
   in
@@ -416,27 +421,21 @@ let declare_structure finite univs id idbuild paramimpls params arity template
     }
   in
   let mie =
-    if poly then
-      begin
+    match ctx with
+    | Polymorphic_const_entry ctx ->
         let env = Global.env () in
         let env' = Environ.push_context ctx env in
         let evd = Evd.from_env env' in
         Inductiveops.infer_inductive_subtyping env' evd mie
-      end
-    else
+    | Monomorphic_const_entry _ ->
        mie
   in
-  let kn = Command.declare_mutual_inductive_with_eliminations mie [] [(paramimpls,[])] in
+  let kn = Command.declare_mutual_inductive_with_eliminations mie ubinders [(paramimpls,[])] in
   let rsp = (kn,0) in (* This is ind path of idstruc *)
   let cstr = (rsp,1) in
-  let fields =
-    if poly then
-      let subst, _ = Univ.abstract_universes ctx in
-      Context.Rel.map (fun c -> Vars.subst_univs_level_constr subst c) fields
-    else fields
-  in
-  let kinds,sp_projs = declare_projections rsp ~kind binder_name coers fieldimpls fields in
+  let kinds,sp_projs = declare_projections rsp ctx ~kind binder_name coers ubinders fieldimpls fields in
   let build = ConstructRef cstr in
+  let poly = match ctx with | Polymorphic_const_entry _ -> true | Monomorphic_const_entry _ -> false in
   let () = if is_coe then Class.try_add_new_coercion build ~local:false poly in
   Recordops.declare_structure(rsp,cstr,List.rev kinds,List.rev sp_projs);
   rsp
@@ -450,7 +449,7 @@ let implicits_of_context ctx =
     in ExplByPos (i, explname), (true, true, true))
     1 (List.rev (Anonymous :: (List.map RelDecl.get_name ctx)))
 
-let declare_class finite def cum poly ctx id idbuild paramimpls params arity 
+let declare_class finite def cum ubinders univs id idbuild paramimpls params arity
     template fieldimpls fields ?(kind=StructureComponent) is_coe coers priorities sign =
   let fieldimpls =
     (* Make the class implicit in the projections, and the params if applicable. *)
@@ -465,27 +464,29 @@ let declare_class finite def cum poly ctx id idbuild paramimpls params arity
       let class_body = it_mkLambda_or_LetIn field params in
       let class_type = it_mkProd_or_LetIn arity params in
       let class_entry = 
-	Declare.definition_entry ~types:class_type ~poly ~univs:ctx class_body in
+        Declare.definition_entry ~types:class_type ~univs class_body in
       let cst = Declare.declare_constant (snd id)
 	(DefinitionEntry class_entry, IsDefinition Definition)
       in
-      let cstu = (cst, if poly then Univ.UContext.instance ctx else Univ.Instance.empty) in
+      let cstu = (cst, match univs with
+        | Polymorphic_const_entry univs -> Univ.UContext.instance univs
+        | Monomorphic_const_entry _ -> Univ.Instance.empty)
+      in
       let inst_type = appvectc (mkConstU cstu)
 			       (Termops.rel_vect 0 (List.length params)) in
       let proj_type =
 	it_mkProd_or_LetIn (mkProd(Name binder_name, inst_type, lift 1 field)) params in
       let proj_body =
 	it_mkLambda_or_LetIn (mkLambda (Name binder_name, inst_type, mkRel 1)) params in
-      let proj_entry =
-	Declare.definition_entry ~types:proj_type ~poly
-	    ~univs:(if poly then ctx else Univ.UContext.empty) proj_body
-      in
+      let proj_entry = Declare.definition_entry ~types:proj_type ~univs proj_body in
       let proj_cst = Declare.declare_constant proj_name
         (DefinitionEntry proj_entry, IsDefinition Definition)
       in
       let cref = ConstRef cst in
       Impargs.declare_manual_implicits false cref [paramimpls];
+      Universes.register_universe_binders cref ubinders;
       Impargs.declare_manual_implicits false (ConstRef proj_cst) [List.hd fieldimpls];
+      Universes.register_universe_binders (ConstRef proj_cst) ubinders;
       Classes.set_typeclass_transparency (EvalConstRef cst) false false;
       let sub = match List.hd coers with
 	| Some b -> Some ((if b then Backward else Forward), List.hd priorities) 
@@ -494,15 +495,16 @@ let declare_class finite def cum poly ctx id idbuild paramimpls params arity
       cref, [Name proj_name, sub, Some proj_cst]
     | _ ->
        let univs =
-         if poly then
+         match univs with
+         | Polymorphic_const_entry univs ->
            if cum then
-             Cumulative_ind_entry (Universes.univ_inf_ind_from_universe_context ctx)
+             Cumulative_ind_entry (Universes.univ_inf_ind_from_universe_context univs)
            else
-             Polymorphic_ind_entry ctx
-         else
-           Monomorphic_ind_entry ctx
+             Polymorphic_ind_entry univs
+         | Monomorphic_const_entry univs ->
+           Monomorphic_ind_entry univs
        in
-       let ind = declare_structure BiFinite univs (snd id) idbuild paramimpls
+       let ind = declare_structure BiFinite ubinders univs (snd id) idbuild paramimpls
 	  params arity template fieldimpls fields
 	  ~kind:Method ~name:binder_name false (List.map (fun _ -> false) fields) sign
        in
@@ -523,13 +525,15 @@ let declare_class finite def cum poly ctx id idbuild paramimpls params arity
       params, params
   in
   let univs, ctx_context, fields =
-    if poly then
-      let usubst, auctx = Univ.abstract_universes ctx in
+    match univs with
+    | Polymorphic_const_entry univs ->
+      let usubst, auctx = Univ.abstract_universes univs in
       let map c = Vars.subst_univs_level_constr usubst c in
       let fields = Context.Rel.map map fields in
       let ctx_context = on_snd (fun d -> Context.Rel.map map d) ctx_context in
       auctx, ctx_context, fields
-    else Univ.AUContext.empty, ctx_context, fields
+    | Monomorphic_const_entry _ ->
+      Univ.AUContext.empty, ctx_context, fields
   in
   let k =
     { cl_univs = univs;
@@ -605,14 +609,14 @@ let definition_structure (kind,cum,poly,finite,(is_coe,((loc,idstruc),pl)),ps,cf
   if isnot_class && List.exists (fun opt -> not (Option.is_empty opt)) priorities then
     user_err Pp.(str "Priorities only allowed for type class substructures");
   (* Now, younger decl in params and fields is on top *)
-  let (pl, ctx), arity, template, implpars, params, implfs, fields =
+  let pl, univs, arity, template, implpars, params, implfs, fields =
     States.with_state_protection (fun () ->
-      typecheck_params_and_fields finite (kind = Class true) idstruc pl s ps notations fs) () in
+      typecheck_params_and_fields finite (kind = Class true) idstruc poly pl s ps notations fs) () in
   let sign = structure_signature (fields@params) in
-  let gr = match kind with
+  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 poly ctx (loc,idstruc) idbuild
+     let gr = declare_class finite def cum pl univs (loc,idstruc) idbuild
 	  implpars params arity template implfs fields is_coe coers priorities sign in
 	gr
     | _ ->
@@ -621,18 +625,16 @@ let definition_structure (kind,cum,poly,finite,(is_coe,((loc,idstruc),pl)),ps,cf
 	           (succ (List.length params)) impls) implfs 
       in
       let univs =
-        if poly then
+        match univs with
+        | Polymorphic_const_entry univs ->
           if cum then
-            Cumulative_ind_entry (Universes.univ_inf_ind_from_universe_context ctx)
+            Cumulative_ind_entry (Universes.univ_inf_ind_from_universe_context univs)
           else
-            Polymorphic_ind_entry ctx
-        else
-          Monomorphic_ind_entry ctx
+            Polymorphic_ind_entry univs
+        | Monomorphic_const_entry univs ->
+          Monomorphic_ind_entry univs
       in
-      let ind = declare_structure finite univs idstruc
+      let ind = declare_structure finite pl univs idstruc
 	  idbuild implpars params arity template implfs 
 	  fields is_coe (List.map (fun coe -> not (Option.is_empty coe)) coers) sign in
 	IndRef ind
-  in
-  Universes.register_universe_binders gr pl;
-  gr
diff --git a/vernac/record.mli b/vernac/record.mli
index 33c2fba89..9fdd5e1c4 100644
--- a/vernac/record.mli
+++ b/vernac/record.mli
@@ -7,36 +7,12 @@
 (************************************************************************)
 
 open Names
-open Constr
 open Vernacexpr
 open Constrexpr
-open Impargs
 open Globnames
 
 val primitive_flag : bool ref
 
-(** [declare_projections ref name coers params fields] declare projections of
-   record [ref] (if allowed) using the given [name] as argument, and put them
-   as coercions accordingly to [coers]; it returns the absolute names of projections *)
-
-val declare_projections :
-  inductive -> ?kind:Decl_kinds.definition_object_kind -> Id.t ->
-  coercion_flag list -> manual_explicitation list list -> Context.Rel.t ->
-  (Name.t * bool) list * Constant.t option list
-
-val declare_structure :
-  Decl_kinds.recursivity_kind ->
-  Entries.inductive_universes ->
-  Id.t -> Id.t ->
-  manual_explicitation list -> Context.Rel.t -> (** params *) constr -> (** arity *)
-  bool (** template arity ? *) ->
-  Impargs.manual_explicitation list list -> Context.Rel.t -> (** fields *)
-  ?kind:Decl_kinds.definition_object_kind -> ?name:Id.t ->
-  bool -> (** coercion? *)
-  bool list -> (** field coercions *)
-  Evd.evar_map ->
-  inductive
-
 val definition_structure :
   inductive_kind * Decl_kinds.cumulative_inductive_flag * Decl_kinds.polymorphic *
   Decl_kinds.recursivity_kind * ident_decl with_coercion * local_binder_expr list *
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index bdd351901..2f278ceb1 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -1555,8 +1555,8 @@ let vernac_check_may_eval ?loc redexp glopt rc =
   let sigma' = Evarconv.solve_unif_constraints_with_heuristics env sigma' in
   Evarconv.check_problems_are_solved env sigma';
   let sigma',nf = Evarutil.nf_evars_and_universes sigma' in
-  let pl, uctx = Evd.universe_context ~names:[] ~extensible:true sigma' in
-  let env = Environ.push_context uctx (Evarutil.nf_env_evar sigma' env) in
+  let uctx = Evd.universe_context_set sigma' in
+  let env = Environ.push_context_set uctx (Evarutil.nf_env_evar sigma' env) in
   let c = nf c in
   let j =
     if Evarutil.has_undefined_evars sigma' (EConstr.of_constr c) then
@@ -1572,7 +1572,7 @@ let vernac_check_may_eval ?loc redexp glopt rc =
         let j = { j with Environ.uj_type = Reductionops.nf_betaiota sigma' j.Environ.uj_type } in
 	Feedback.msg_notice (print_judgment env sigma' j ++
                     pr_ne_evar_set (fnl () ++ str "where" ++ fnl ()) (mt ()) sigma' l ++
-                    Printer.pr_universe_ctx sigma uctx)
+                    Printer.pr_universe_ctx_set sigma uctx)
     | Some r ->
         let (sigma',r_interp) = Hook.get f_interp_redexp env sigma' r in
 	let redfun env evm c =
@@ -1609,9 +1609,10 @@ exception NoHyp
 (* Printing "About" information of a hypothesis of the current goal.
    We only print the type and a small statement to this comes from the
    goal. Precondition: there must be at least one current goal. *)
-let print_about_hyp_globs ?loc ref_or_by_not glopt =
+let print_about_hyp_globs ?loc ref_or_by_not udecl glopt =
   let open Context.Named.Declaration in
   try
+    (* FIXME error on non None udecl if we find the hyp. *)
     let glnumopt = query_command_selector ?loc glopt in
     let gl,id =
       match glnumopt,ref_or_by_not with
@@ -1634,7 +1635,7 @@ let print_about_hyp_globs ?loc ref_or_by_not glopt =
   with (* fallback to globals *)
     | NoHyp | Not_found ->
     let sigma, env = Pfedit.get_current_context () in
-    print_about env sigma ref_or_by_not
+    print_about env sigma ref_or_by_not udecl
 
 
 let vernac_print ?loc env sigma = let open Feedback in function
@@ -1651,7 +1652,7 @@ let vernac_print ?loc env sigma = let open Feedback in function
   | PrintMLLoadPath -> msg_notice (Mltop.print_ml_path ())
   | PrintMLModules -> msg_notice (Mltop.print_ml_modules ())
   | PrintDebugGC -> msg_notice (Mltop.print_gc ())
-  | PrintName qid -> dump_global qid; msg_notice (print_name env sigma qid)
+  | PrintName (qid,udecl) -> dump_global qid; msg_notice (print_name env sigma qid udecl)
   | PrintGraph -> msg_notice (Prettyp.print_graph())
   | PrintClasses -> msg_notice (Prettyp.print_classes())
   | PrintTypeClasses -> msg_notice (Prettyp.print_typeclasses())
@@ -1681,8 +1682,8 @@ let vernac_print ?loc env sigma = let open Feedback in function
       msg_notice (Notation.pr_scope (Constrextern.without_symbols (pr_lglob_constr_env env)) s)
   | PrintVisibility s ->
       msg_notice (Notation.pr_visibility (Constrextern.without_symbols (pr_lglob_constr_env env)) s)
-  | PrintAbout (ref_or_by_not,glnumopt) ->
-     msg_notice (print_about_hyp_globs ?loc ref_or_by_not glnumopt)
+  | PrintAbout (ref_or_by_not,udecl,glnumopt) ->
+     msg_notice (print_about_hyp_globs ?loc ref_or_by_not udecl glnumopt)
   | PrintImplicit qid ->
     dump_global qid; msg_notice (print_impargs qid)
   | PrintAssumptions (o,t,r) ->