Use Entries.constant_universes_entry more.

This reduces conversions between ContextSet/UContext and encodes
whether we are polymorphic by which constructor we use rather than
using some boolean.

22 files changed, 251 insertions, 198 deletions

diff --git a/API/API.mli b/API/API.mli
index ad5d5490b..4405bf8da 100644
--- a/API/API.mli
+++ b/API/API.mli
@@ -2764,6 +2764,9 @@ sig
   val context_set : t -> Univ.ContextSet.t
   val of_context_set : Univ.ContextSet.t -> t
 
+  val const_univ_entry : poly:bool -> t -> Entries.constant_universes_entry
+  val ind_univ_entry : poly:bool -> t -> Entries.inductive_universes
+
   type rigid =
     | UnivRigid
     | UnivFlexible of bool
@@ -2887,6 +2890,8 @@ sig
     val from_ctx : UState.t -> evar_map
 
     val to_universe_context : evar_map -> Univ.UContext.t
+    val const_univ_entry : poly:bool -> evar_map -> Entries.constant_universes_entry
+    val ind_univ_entry : poly:bool -> evar_map -> Entries.inductive_universes
 
     val meta_list : evar_map -> (Constr.metavariable * clbinding) list
 
@@ -4669,11 +4674,11 @@ sig
 
   val declare_definition :
     ?internal:internal_flag -> ?opaque:bool -> ?kind:Decl_kinds.definition_object_kind ->
-    ?local:bool -> ?poly:Decl_kinds.polymorphic -> Names.Id.t -> ?types:Constr.t ->
-    Constr.t Univ.in_universe_context_set -> Names.Constant.t
+    ?local:bool -> Names.Id.t -> ?types:Constr.t ->
+    Constr.t Entries.in_constant_universes_entry -> Names.Constant.t
   val definition_entry : ?fix_exn:Future.fix_exn ->
     ?opaque:bool -> ?inline:bool -> ?types:Constr.types ->
-    ?poly:Decl_kinds.polymorphic -> ?univs:Univ.UContext.t ->
+    ?univs:Entries.constant_universes_entry ->
     ?eff:Safe_typing.private_constants -> Constr.t -> Safe_typing.private_constants Entries.definition_entry
   val definition_message : Names.Id.t -> unit
   val declare_variable : Names.Id.t -> variable_declaration -> Libnames.object_name
diff --git a/engine/evd.ml b/engine/evd.ml
index eb0f2e3e7..9ea2cc00f 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -758,7 +758,10 @@ let universe_context_set d = UState.context_set d.universes
 
 let to_universe_context evd = UState.context evd.universes
 
-let check_univ_decl evd decl = UState.check_univ_decl evd.universes decl
+let const_univ_entry ~poly evd = UState.const_univ_entry ~poly evd.universes
+let ind_univ_entry ~poly evd = UState.ind_univ_entry ~poly evd.universes
+
+let check_univ_decl ~poly evd decl = UState.check_univ_decl ~poly evd.universes decl
 
 let restrict_universe_context evd vars =
   { evd with universes = UState.restrict evd.universes vars }
diff --git a/engine/evd.mli b/engine/evd.mli
index 49b6a7583..f06fb8d3b 100644
--- a/engine/evd.mli
+++ b/engine/evd.mli
@@ -562,8 +562,12 @@ val universes : evar_map -> UGraph.t
     [Univ.ContextSet.to_context]. *)
 val to_universe_context : evar_map -> Univ.UContext.t
 
-val check_univ_decl : evar_map -> UState.universe_decl ->
-  Univ.UContext.t
+val const_univ_entry : poly:bool -> evar_map -> Entries.constant_universes_entry
+
+(** NB: [ind_univ_entry] cannot create cumulative entries. *)
+val ind_univ_entry : poly:bool -> evar_map -> Entries.inductive_universes
+
+val check_univ_decl : poly:bool -> evar_map -> UState.universe_decl -> Entries.constant_universes_entry
 
 val merge_universe_context : evar_map -> UState.t -> evar_map
 val set_universe_context : evar_map -> UState.t -> evar_map
diff --git a/engine/uState.ml b/engine/uState.ml
index ff91493ee..dadc004c5 100644
--- a/engine/uState.ml
+++ b/engine/uState.ml
@@ -87,6 +87,17 @@ let constraints ctx = snd ctx.uctx_local
 
 let context ctx = Univ.ContextSet.to_context ctx.uctx_local
 
+let const_univ_entry ~poly uctx =
+  let open Entries in
+  if poly then Polymorphic_const_entry (context uctx)
+  else Monomorphic_const_entry (context_set uctx)
+
+(* does not support cumulativity since you need more info *)
+let ind_univ_entry ~poly uctx =
+  let open Entries in
+  if poly then Polymorphic_ind_entry (context uctx)
+  else Monomorphic_ind_entry (context_set uctx)
+
 let of_context_set ctx = { empty with uctx_local = ctx }
 
 let subst ctx = ctx.uctx_univ_variables
@@ -260,58 +271,92 @@ let pr_uctx_level uctx =
 type universe_decl =
   (Names.Id.t Loc.located list, Univ.Constraint.t) Misctypes.gen_universe_decl
 
+let error_unbound_universes left uctx =
+  let open Univ in
+  let n = LSet.cardinal left in
+  let loc =
+    try
+      let info =
+        LMap.find (LSet.choose left) (snd uctx.uctx_names) in
+      info.uloc
+    with Not_found -> None
+  in
+  user_err ?loc ~hdr:"universe_context"
+    ((str(CString.plural n "Universe") ++ spc () ++
+      LSet.pr (pr_uctx_level uctx) left ++
+      spc () ++ str (CString.conjugate_verb_to_be n) ++
+      str" unbound."))
+
 let universe_context ~names ~extensible uctx =
-  let levels = Univ.ContextSet.levels uctx.uctx_local in
+  let open Univ in
+  let levels = ContextSet.levels uctx.uctx_local in
   let newinst, left =
     List.fold_right
       (fun (loc,id) (newinst, acc) ->
          let l =
            try UNameMap.find id (fst uctx.uctx_names)
-           with Not_found ->
-             user_err ?loc ~hdr:"universe_context"
-               (str"Universe " ++ Id.print id ++ str" is not bound anymore.")
-         in (l :: newinst, Univ.LSet.remove l acc))
+           with Not_found -> assert false
+         in (l :: newinst, LSet.remove l acc))
       names ([], levels)
   in
-  if not extensible && not (Univ.LSet.is_empty left) then
-    let n = Univ.LSet.cardinal left in
-    let loc =
-      try
-        let info =
-          Univ.LMap.find (Univ.LSet.choose left) (snd uctx.uctx_names) in
-        info.uloc
-      with Not_found -> None
-    in
-    user_err ?loc ~hdr:"universe_context"
-      ((str(CString.plural n "Universe") ++ spc () ++
-        Univ.LSet.pr (pr_uctx_level uctx) left ++
-	spc () ++ str (CString.conjugate_verb_to_be n) ++
-        str" unbound."))
+  if not extensible && not (LSet.is_empty left)
+  then error_unbound_universes left uctx
   else
-    let left = Univ.ContextSet.sort_levels (Array.of_list (Univ.LSet.elements left)) in
+    let left = ContextSet.sort_levels (Array.of_list (LSet.elements left)) in
     let inst = Array.append (Array.of_list newinst) left in
-    let inst = Univ.Instance.of_array inst in
-    let ctx = Univ.UContext.make (inst,
-                                  Univ.ContextSet.constraints uctx.uctx_local) in
+    let inst = Instance.of_array inst in
+    let ctx = UContext.make (inst, ContextSet.constraints uctx.uctx_local) in
     ctx
 
-let check_implication uctx cstrs ctx =
+let check_universe_context_set ~names ~extensible uctx =
+  if extensible then ()
+  else
+    let open Univ in
+    let left = List.fold_left (fun left (loc,id) ->
+        let l =
+          try UNameMap.find id (fst uctx.uctx_names)
+          with Not_found -> assert false
+        in LSet.remove l left)
+        (ContextSet.levels uctx.uctx_local) names
+    in
+    if not (LSet.is_empty left)
+    then error_unbound_universes left uctx
+
+let check_implication uctx cstrs cstrs' =
   let gr = initial_graph uctx in
   let grext = UGraph.merge_constraints cstrs gr in
-  let cstrs' = Univ.UContext.constraints ctx in
   if UGraph.check_constraints cstrs' grext then ()
   else CErrors.user_err ~hdr:"check_univ_decl"
       (str "Universe constraints are not implied by the ones declared.")
 
-let check_univ_decl uctx decl =
+let check_mono_univ_decl uctx decl =
+  let open Misctypes in
+  let () =
+    let names = decl.univdecl_instance in
+    let extensible = decl.univdecl_extensible_instance in
+    check_universe_context_set ~names ~extensible uctx
+  in
+  if not decl.univdecl_extensible_constraints then
+    check_implication uctx
+      decl.univdecl_constraints
+      (Univ.ContextSet.constraints uctx.uctx_local);
+  uctx.uctx_local
+
+let check_univ_decl ~poly uctx decl =
   let open Misctypes in
-  let ctx = universe_context
-      ~names:decl.univdecl_instance
-      ~extensible:decl.univdecl_extensible_instance
-      uctx
+  let ctx =
+    let names = decl.univdecl_instance in
+    let extensible = decl.univdecl_extensible_instance in
+    if poly
+    then Entries.Polymorphic_const_entry (universe_context ~names ~extensible uctx)
+    else
+      let () = check_universe_context_set ~names ~extensible uctx in
+      Entries.Monomorphic_const_entry uctx.uctx_local
   in
   if not decl.univdecl_extensible_constraints then
-    check_implication uctx decl.univdecl_constraints ctx;
+    check_implication uctx
+      decl.univdecl_constraints
+      (Univ.ContextSet.constraints uctx.uctx_local);
   ctx
 
 let restrict ctx vars =
diff --git a/engine/uState.mli b/engine/uState.mli
index 5279c6388..4265f2b20 100644
--- a/engine/uState.mli
+++ b/engine/uState.mli
@@ -59,6 +59,13 @@ val constraints : t -> Univ.constraints
 val context : t -> Univ.UContext.t
 (** Shorthand for {!context_set} with {!Context_set.to_context}. *)
 
+val const_univ_entry : poly:bool -> t -> Entries.constant_universes_entry
+(** Pick from {!context} or {!context_set} based on [poly]. *)
+
+val ind_univ_entry : poly:bool -> t -> Entries.inductive_universes
+(** Pick from {!context} or {!context_set} based on [poly].
+    Cannot create cumulative entries. *)
+
 (** {5 Constraints handling} *)
 
 val add_constraints : t -> Univ.constraints -> t
@@ -133,11 +140,15 @@ type universe_decl =
    If non extensible in [decl], check that the local universes (resp.
    universe constraints) in [ctx] are implied by [decl].
 
-   Return a universe context containing the local universes of [ctx]
-   and their constraints. The universes corresponding to
+   Return a [Entries.constant_universes_entry] containing the local
+   universes of [ctx] and their constraints.
+
+   When polymorphic, the universes corresponding to
    [decl.univdecl_instance] come first in the order defined by that
    list. *)
-val check_univ_decl : t -> universe_decl -> Univ.UContext.t
+val check_univ_decl : poly:bool -> t -> universe_decl -> Entries.constant_universes_entry
+
+val check_mono_univ_decl : t -> universe_decl -> Univ.ContextSet.t
 
 (** {5 TODO: Document me} *)
 
diff --git a/interp/declare.ml b/interp/declare.ml
index 15999f1d1..1b4645aff 100644
--- a/interp/declare.ml
+++ b/interp/declare.ml
@@ -203,14 +203,9 @@ let declare_constant_common id cst =
   update_tables c;
   c
 
+let default_univ_entry = Monomorphic_const_entry Univ.ContextSet.empty
 let definition_entry ?fix_exn ?(opaque=false) ?(inline=false) ?types
-    ?(poly=false) ?(univs=Univ.UContext.empty) ?(eff=Safe_typing.empty_private_constants) body =
-  let univs =
-    if poly then Polymorphic_const_entry univs
-    else
-      (* FIXME be smarter about this *)
-      Monomorphic_const_entry (Univ.ContextSet.of_context univs)
-  in
+    ?(univs=default_univ_entry) ?(eff=Safe_typing.empty_private_constants) body =
   { const_entry_body = Future.from_val ?fix_exn ((body,Univ.ContextSet.empty), eff);
     const_entry_secctx = None;
     const_entry_type = types;
@@ -263,9 +258,9 @@ let declare_constant ?(internal = UserIndividualRequest) ?(local = false) id ?(e
 
 let declare_definition ?(internal=UserIndividualRequest)
   ?(opaque=false) ?(kind=Decl_kinds.Definition) ?(local = false)
-  ?(poly=false) id ?types (body,ctx) =
+  id ?types (body,univs) =
   let cb =
-    definition_entry ?types ~poly ~univs:(Univ.ContextSet.to_context ctx) ~opaque body
+    definition_entry ?types ~univs ~opaque body
   in
     declare_constant ~internal ~local id
       (Entries.DefinitionEntry cb, Decl_kinds.IsDefinition kind)
diff --git a/interp/declare.mli b/interp/declare.mli
index 9b3194dec..d50d37368 100644
--- a/interp/declare.mli
+++ b/interp/declare.mli
@@ -42,7 +42,7 @@ type internal_flag =
 (* Defaut definition entries, transparent with no secctx or proj information *)
 val definition_entry : ?fix_exn:Future.fix_exn ->
   ?opaque:bool -> ?inline:bool -> ?types:types ->
-  ?poly:polymorphic -> ?univs:Univ.UContext.t ->
+  ?univs:Entries.constant_universes_entry ->
   ?eff:Safe_typing.private_constants -> constr -> Safe_typing.private_constants definition_entry
 
 (** [declare_constant id cd] declares a global declaration
@@ -56,8 +56,8 @@ val declare_constant :
 
 val declare_definition : 
   ?internal:internal_flag -> ?opaque:bool -> ?kind:definition_object_kind ->
-  ?local:bool -> ?poly:polymorphic -> Id.t -> ?types:constr -> 
-  constr Univ.in_universe_context_set -> Constant.t
+  ?local:bool -> Id.t -> ?types:constr ->
+  constr Entries.in_constant_universes_entry -> Constant.t
 
 (** Since transparent constants' side effects are globally declared, we
  *  need that *)
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index 076fba861..7a9bbd92c 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -348,8 +348,11 @@ let generate_functional_principle (evd: Evd.evar_map ref)
         let evd',value = change_property_sort evd' s new_principle_type new_princ_name in
         let evd' = fst (Typing.type_of ~refresh:true (Global.env ()) evd' (EConstr.of_constr value)) in
         (* Pp.msgnl (str "new principle := " ++ pr_lconstr value); *)
-        let univs = Evd.to_universe_context evd' in
-        let ce = Declare.definition_entry ~poly:(Flags.is_universe_polymorphism ()) ~univs value in
+        let univs =
+          let poly = Flags.is_universe_polymorphism () in
+          Evd.const_univ_entry ~poly evd'
+        in
+        let ce = Declare.definition_entry ~univs value in
 	ignore(
 	  Declare.declare_constant
 	    name
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 320f7c7f3..b0a76137b 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -66,8 +66,8 @@ let find_reference sl s =
   let dp = Names.DirPath.make (List.rev_map Id.of_string sl) in
   locate (make_qualid dp (Id.of_string s))
 
-let declare_fun f_id kind ?(ctx=Univ.UContext.empty) value =
-  let ce = definition_entry ~univs:ctx value (*FIXME *) in
+let declare_fun f_id kind ?univs value =
+  let ce = definition_entry ?univs value (*FIXME *) in
     ConstRef(declare_constant f_id (DefinitionEntry ce, kind));;
 
 let defined () = Lemmas.save_proof (Vernacexpr.(Proved (Transparent,None)))
@@ -1556,8 +1556,8 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num
   let functional_id =  add_suffix function_name "_F" in
   let term_id = add_suffix function_name "_terminate" in
   let functional_ref =
-    let ctx = Evd.to_universe_context evm in
-    declare_fun functional_id (IsDefinition Decl_kinds.Definition) ~ctx res
+    let univs = Entries.Monomorphic_const_entry (Evd.universe_context_set evm) in
+    declare_fun functional_id (IsDefinition Decl_kinds.Definition) ~univs res
   in
   (* Refresh the global universes, now including those of _F *)
   let evm = Evd.from_env (Global.env ()) in
diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4
index d6cfa3cf9..750517e91 100644
--- a/plugins/ltac/extratactics.ml4
+++ b/plugins/ltac/extratactics.ml4
@@ -313,10 +313,10 @@ let project_hint pri l2r r =
   let id =
     Nameops.add_suffix (Nametab.basename_of_global gr) ("_proj_" ^ (if l2r then "l2r" else "r2l"))
   in
-  let ctx = Evd.universe_context_set sigma in
-  let c = EConstr.to_constr sigma c in
   let poly = Flags.use_polymorphic_flag () in
-  let c = Declare.declare_definition ~poly ~internal:Declare.InternalTacticRequest id (c,ctx) in
+  let ctx = Evd.const_univ_entry ~poly sigma in
+  let c = EConstr.to_constr sigma c in
+  let c = Declare.declare_definition ~internal:Declare.InternalTacticRequest id (c,ctx) in
   let info = {Vernacexpr.hint_priority = pri; hint_pattern = None} in
     (info,false,true,Hints.PathAny, Hints.IsGlobRef (Globnames.ConstRef c))
 
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index a2f5a4577..c0060c5a7 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -1884,11 +1884,11 @@ let declare_projection n instance_id r =
     in it_mkProd_or_LetIn ccl ctx
   in
   let typ = it_mkProd_or_LetIn typ ctx in
-  let ctx = Evd.to_universe_context sigma in
+  let univs = Evd.const_univ_entry ~poly sigma in
   let typ = EConstr.to_constr sigma typ in
   let term = EConstr.to_constr sigma term in
   let cst = 
-    Declare.definition_entry ~types:typ ~poly ~univs:ctx term
+    Declare.definition_entry ~types:typ ~univs term
   in
     ignore(Declare.declare_constant n 
 	   (Entries.DefinitionEntry cst, Decl_kinds.IsDefinition Decl_kinds.Definition))
@@ -1972,10 +1972,7 @@ let add_morphism_infer glob m n =
   let evd = Evd.from_env env in
   let uctx, instance = build_morphism_signature env evd m in
     if Lib.is_modtype () then
-      let uctx = if poly
-        then Entries.Polymorphic_const_entry (UState.context uctx)
-        else Entries.Monomorphic_const_entry (UState.context_set uctx)
-      in
+      let uctx = UState.const_univ_entry ~poly uctx in
       let cst = Declare.declare_constant ~internal:Declare.InternalTacticRequest instance_id
 				(Entries.ParameterEntry 
                                  (None,(instance,uctx),None),
diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml
index 6d0b6fd09..f22f00839 100644
--- a/plugins/setoid_ring/newring.ml
+++ b/plugins/setoid_ring/newring.ml
@@ -150,13 +150,13 @@ let ic_unsafe c = (*FIXME remove *)
   let sigma = Evd.from_env env in
     EConstr.of_constr (fst (Constrintern.interp_constr env sigma c))
 
-let decl_constant na ctx c =
+let decl_constant na univs c =
   let open Constr in
   let vars = Univops.universes_of_constr c in
-  let ctx = Univops.restrict_universe_context (Univ.ContextSet.of_context ctx) vars in
+  let univs = Univops.restrict_universe_context univs vars in
+  let univs = Monomorphic_const_entry univs in
   mkConst(declare_constant (Id.of_string na) 
-	    (DefinitionEntry (definition_entry ~opaque:true
-				~univs:(Univ.ContextSet.to_context ctx) c),
+            (DefinitionEntry (definition_entry ~opaque:true ~univs c),
 	     IsProof Lemma))
 
 (* Calling a global tactic *)
@@ -220,7 +220,7 @@ let exec_tactic env evd n f args =
   let gls = Proofview.V82.of_tactic (Tacinterp.eval_tactic_ist ist (ltac_call f (args@[getter]))) gl in
   let evd, nf = Evarutil.nf_evars_and_universes (Refiner.project gls) in
   let nf c = nf (constr_of c) in
-  Array.map nf !tactic_res, Evd.to_universe_context evd
+  Array.map nf !tactic_res, Evd.universe_context_set evd
 
 let stdlib_modules =
   [["Coq";"Setoids";"Setoid"];
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index 905173efc..bfd64e21b 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -316,10 +316,6 @@ let get_open_goals () =
     (List.map (fun (l1,l2) -> List.length l1 + List.length l2) gll) +
     List.length shelf
 
-let constrain_variables init uctx =
-  let levels = Univ.Instance.levels (Univ.UContext.instance init) in
-  UState.constrain_variables levels uctx
-
 type closed_proof_output = (Constr.t * Safe_typing.private_constants) list * UState.t
 
 let close_proof ~keep_body_ucst_separate ?feedback_id ~now
@@ -329,9 +325,12 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now
   let poly = pi2 strength (* Polymorphic *) in
   let initial_goals = Proof.initial_goals proof in
   let initial_euctx = Proof.initial_euctx proof in
+  let constrain_variables ctx =
+    UState.constrain_variables (fst (UState.context_set initial_euctx)) ctx
+  in
   let fpl, univs = Future.split2 fpl in
   let universes = if poly || now then Future.force univs else initial_euctx in
-  let univctx = UState.check_univ_decl universes universe_decl in
+  let univctx = UState.check_univ_decl ~poly universes universe_decl 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
@@ -353,15 +352,15 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now
         let used_univs_typ = Univops.universes_of_constr typ in
         if keep_body_ucst_separate ||
            not (Safe_typing.empty_private_constants = eff) then
-          let initunivs = UState.context initial_euctx in
-          let ctx = constrain_variables initunivs universes in
+          let initunivs = UState.const_univ_entry ~poly initial_euctx in
+          let ctx = constrain_variables universes in
           (* For vi2vo compilation proofs are computed now but we need to
              complement the univ constraints of the typ with the ones of
              the body.  So we keep the two sets distinct. *)
 	  let used_univs = Univ.LSet.union used_univs_body used_univs_typ in
           let ctx_body = UState.restrict ctx used_univs in
-          let univs = UState.check_univ_decl ctx_body universe_decl in
-          (initunivs, typ), ((body, Univ.ContextSet.of_context univs), eff)
+          let univs = UState.check_mono_univ_decl ctx_body universe_decl in
+          (initunivs, typ), ((body, univs), eff)
         else
           (* Since the proof is computed now, we can simply have 1 set of
              constraints in which we merge the ones for the body and the ones
@@ -370,7 +369,7 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now
              TODO: check if restrict is really necessary now. *)
           let used_univs = Univ.LSet.union used_univs_body used_univs_typ in
           let ctx = UState.restrict universes used_univs in
-          let univs = UState.check_univ_decl ctx universe_decl in
+          let univs = UState.check_univ_decl ~poly ctx universe_decl in
           (univs, typ), ((body, Univ.ContextSet.empty), eff)
       in 
        fun t p -> Future.split2 (Future.chain p (make_body t))
@@ -382,20 +381,14 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now
              the initial universes, ensure that the final universes respect
              the declaration as well. If the declaration is non-extensible,
              this will prevent the body from adding universes and constraints. *)
-          let bodyunivs = constrain_variables univctx (Future.force univs) in
-          let univs = UState.check_univ_decl bodyunivs universe_decl in
-          (pt,Univ.ContextSet.of_context univs),eff)
+          let bodyunivs = constrain_variables (Future.force univs) in
+          let univs = UState.check_mono_univ_decl bodyunivs universe_decl in
+          (pt,univs),eff)
   in
   let entry_fn p (_, t) =
     let t = EConstr.Unsafe.to_constr t in
     let univstyp, body = make_body t p in
     let univs, typ = Future.force univstyp in
-    let univs =
-      if poly then Entries.Polymorphic_const_entry univs
-      else
-        (* FIXME be smarter about the unnecessary context linearisation in make_body *)
-        Entries.Monomorphic_const_entry (Univ.ContextSet.of_context univs)
-    in
     {Entries.
       const_entry_body = body;
       const_entry_secctx = section_vars;
diff --git a/tactics/leminv.ml b/tactics/leminv.ml
index 1ee873e0f..1ae3577ed 100644
--- a/tactics/leminv.ml
+++ b/tactics/leminv.ml
@@ -232,12 +232,15 @@ let inversion_scheme env sigma t sort dep_option inv_op =
   let invProof = it_mkNamedLambda_or_LetIn c !ownSign in
   let invProof = EConstr.Unsafe.to_constr invProof in
   let p = Evarutil.nf_evars_universes sigma invProof in
-    p, Evd.to_universe_context sigma
+    p, sigma
 
 let add_inversion_lemma name env sigma t sort dep inv_op =
-  let invProof, univs = inversion_scheme env sigma t sort dep inv_op in
-  let entry = definition_entry ~poly:(Flags.use_polymorphic_flag ())
-                               ~univs invProof in
+  let invProof, sigma = inversion_scheme env sigma t sort dep inv_op in
+  let univs =
+    let poly = Flags.use_polymorphic_flag () in
+    Evd.const_univ_entry ~poly sigma
+  in
+  let entry = definition_entry ~univs invProof in
   let _ = declare_constant name (DefinitionEntry entry, IsProof Lemma) in
   ()
 
diff --git a/vernac/class.ml b/vernac/class.ml
index 68fd22cb6..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 = Evd.to_universe_context 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 c99eba2cc..1833b7a1d 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -119,9 +119,9 @@ 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 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
@@ -203,16 +203,10 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance)
             nf t
         in
         Pretyping.check_evars env Evd.empty !evars (EConstr.of_constr termtype);
-        let ctx = Evd.check_univ_decl !evars decl in
-        let ctx = if poly
-          then Polymorphic_const_entry ctx
-          else
-            (* FIXME be smarter about this *)
-            Monomorphic_const_entry (Univ.ContextSet.of_context ctx)
-        in
+        let univs = Evd.check_univ_decl ~poly !evars decl in
         let cst = Declare.declare_constant ~internal:Declare.InternalTacticRequest id
           (ParameterEntry
-            (None,(termtype,ctx),None), Decl_kinds.IsAssumption Decl_kinds.Logical)
+            (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
@@ -391,19 +385,16 @@ let context poly l =
   let fn status (id, b, t) =
     if Lib.is_modtype () && not (Lib.sections_are_opened ()) then
       (* Declare the universe context once *)
-      let univs = !uctx in
+      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 ->
-        let univs = if poly
-          then Polymorphic_const_entry (Univ.ContextSet.to_context univs)
-          else Monomorphic_const_entry univs
-        in
         (ParameterEntry (None,(t,univs),None), IsAssumption Logical)
       | Some b ->
-        (* FIXME be smarter about this *)
-        let univs = Univ.ContextSet.to_context univs in
-        let entry = Declare.definition_entry ~poly ~univs ~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
@@ -426,9 +417,12 @@ let context poly l =
         pi3 (Command.declare_assumption false decl (t, !uctx) Universes.empty_binders [] impl
           Vernacexpr.NoInline (Loc.tag id))
       | Some b ->
-        let ctx = Univ.ContextSet.to_context !uctx in
+        let univs = if poly
+          then Polymorphic_const_entry (Univ.ContextSet.to_context !uctx)
+          else Monomorphic_const_entry !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 Universes.empty_binders [] hook in
         Lib.sections_are_opened () || Lib.is_modtype_strict ()
diff --git a/vernac/command.ml b/vernac/command.ml
index 06d0c8470..1a8b16a89 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,15 +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 uctx = Evd.check_univ_decl evd decl 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,
-	  definition_entry ~univs:uctx ~poly:p body
+          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
@@ -134,10 +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 uctx = Evd.check_univ_decl ctx decl 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 ~poly:p 
+          definition_entry ~types:typ
 	    ~univs:uctx body
   in
   red_constant_entry (Context.Rel.length ctx) ce !evdref red_option, !evdref, decl, pl, imps
@@ -282,9 +282,14 @@ let do_assumptions_bound_univs coe kind nl id pl c =
   let ty = nf ty in
   let vars = Univops.universes_of_constr ty in
   let evd = Evd.restrict_universe_context !evdref vars in
-  let uctx = Evd.check_univ_decl evd decl in
+  let uctx = Evd.check_univ_decl ~poly:(pi2 kind) evd decl in
   let binders = Evd.universe_binders evd in
-  let uctx = Univ.ContextSet.of_context uctx in
+  let uctx = match uctx with
+    | Polymorphic_const_entry uctx ->
+      (* ?? *)
+      Univ.ContextSet.of_context uctx
+    | Monomorphic_const_entry uctx -> uctx
+  in
   let (_, _, st) = declare_assumption coe kind (ty, uctx) binders impls false nl id in
   st
 
@@ -582,7 +587,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 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,_) ->
@@ -604,12 +609,13 @@ 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_ind_entry (Univ.ContextSet.of_context uctx)
+    | Monomorphic_const_entry uctx ->
+      Monomorphic_ind_entry uctx
   in
   (* Build the mutual inductive entry *)
   let mind_ent =
@@ -1032,9 +1038,9 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation =
         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 !evdref decl in
+        let univs = Evd.check_univ_decl ~poly !evdref decl in
         (*FIXME poly? *)
-        let ce = definition_entry ~poly ~types:ty ~univs (EConstr.to_constr !evdref body) in
+        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
@@ -1173,7 +1179,7 @@ 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 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)
@@ -1206,7 +1212,7 @@ 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 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);
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/lemmas.ml b/vernac/lemmas.ml
index f59b5fcae..a787ec6fa 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -224,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 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 ->
@@ -232,7 +232,13 @@ let save_remaining_recthms (locality,p,kind) norm ctx body opaq i (id,(t_i,(_,im
       | 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 ->
@@ -242,11 +248,7 @@ let save_remaining_recthms (locality,p,kind) norm ctx body opaq i (id,(t_i,(_,im
           | Global -> false
           | Discharge -> assert false
           in
-          let ctx = if p
-            then Polymorphic_const_entry ctx
-            else Monomorphic_const_entry (Univ.ContextSet.of_context ctx)
-          in
-          let decl = (ParameterEntry (None,(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 ->
@@ -264,8 +266,7 @@ let save_remaining_recthms (locality,p,kind) norm ctx body opaq i (id,(t_i,(_,im
       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)
@@ -276,7 +277,7 @@ let save_remaining_recthms (locality,p,kind) norm ctx body opaq i (id,(t_i,(_,im
         | 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)
@@ -425,7 +426,7 @@ 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 ctx decl 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
@@ -460,7 +461,7 @@ let start_proof_com ?inference_hook kind thms hook =
   let () =
     let open Misctypes in
     if not (decl.univdecl_extensible_instance && decl.univdecl_extensible_constraints) then
-       ignore (Evd.check_univ_decl evd decl)
+       ignore (Evd.check_univ_decl ~poly:(pi2 kind) evd decl)
   in
   let evd =
     if pi2 kind then evd
@@ -495,10 +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 = if pi2 k (* polymorphic *)
-              then Polymorphic_const_entry (UState.context (fst universes))
-              else Monomorphic_const_entry (UState.context_set (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, (typ, ctx), None), universes)
         | None ->
@@ -521,12 +519,8 @@ let save_proof ?proof = function
               | _ -> None in
 	    let decl = Proof_global.get_universe_decl () in
             let evd = Evd.from_ctx universes in
-            let ctx = Evd.check_univ_decl evd decl in
             let poly = pi2 k in
-            let ctx = if poly
-              then Polymorphic_const_entry ctx
-              else Monomorphic_const_entry (Univ.ContextSet.of_context ctx)
-            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))
diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index a9110c76c..97cdd7977 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -475,12 +475,8 @@ 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 () = ignore(UState.check_univ_decl prg.prg_ctx prg.prg_univdecl) in
-  let ce =
-    definition_entry ~fix_exn
-     ~opaque ~types:(nf typ) ~poly:(pi2 prg.prg_kind)
-     ~univs:(UState.context prg.prg_ctx) (nf body)
-  in
+  let univs = UState.check_univ_decl ~poly:(pi2 prg.prg_kind) prg.prg_ctx prg.prg_univdecl in
+  let ce = definition_entry ~fix_exn ~opaque ~types:(nf typ) ~univs (nf body) in
   let () = progmap_remove prg in
   let ubinders = UState.universe_binders prg.prg_ctx in
   DeclareDef.declare_definition prg.prg_name
@@ -549,9 +545,9 @@ let declare_mutual_definition l =
             mk_proof (mkCoFix (i,fixdecls))) 0 l
   in
   (* Declare the recursive definitions *)
-  let ctx = UState.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) Universes.empty_binders 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;
@@ -856,10 +852,7 @@ let obligation_terminator name num guard hook auto pf =
         | (_, status), Vernacexpr.Transparent -> status
       in
       let obl = { obl with obl_status = false, status } 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 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
diff --git a/vernac/record.ml b/vernac/record.ml
index faf277d86..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,7 +167,7 @@ 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);
@@ -449,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 ubinders 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. *)
@@ -464,21 +464,21 @@ let declare_class finite def cum poly ubinders ctx id idbuild paramimpls params
       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
@@ -495,13 +495,14 @@ let declare_class finite def cum poly ubinders ctx id idbuild paramimpls params
       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 (Univ.ContextSet.of_context ctx)
+             Polymorphic_ind_entry univs
+         | Monomorphic_const_entry univs ->
+           Monomorphic_ind_entry univs
        in
        let ind = declare_structure BiFinite ubinders univs (snd id) idbuild paramimpls
 	  params arity template fieldimpls fields
@@ -524,13 +525,15 @@ let declare_class finite def cum poly ubinders ctx id idbuild paramimpls params
       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;
@@ -606,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
   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 pl 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
     | _ ->
@@ -622,13 +625,14 @@ 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 (Univ.ContextSet.of_context ctx)
+            Polymorphic_ind_entry univs
+        | Monomorphic_const_entry univs ->
+          Monomorphic_ind_entry univs
       in
       let ind = declare_structure finite pl univs idstruc
 	  idbuild implpars params arity template implfs