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.

8 files changed, 97 insertions, 103 deletions

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