More precise type for universe entries.

We use an algebraic type instead of a pair of a boolean and the corresponding
data. For now, this is isomorphic, but this allows later change in the structure.

12 files changed, 77 insertions, 36 deletions

diff --git a/API/API.mli b/API/API.mli
index bb24d5768..4d9904b5f 100644
--- a/API/API.mli
+++ b/API/API.mli
@@ -1345,6 +1345,9 @@ sig
   type inline = int option
   type 'a proof_output = Constr.t Univ.in_universe_context_set * 'a
   type 'a const_entry_body = 'a proof_output Future.computation
+  type constant_universes_entry =
+    | Monomorphic_const_entry of Univ.universe_context
+    | Polymorphic_const_entry of Univ.universe_context
   type 'a definition_entry =
                                { const_entry_body   : 'a const_entry_body;
                                  (* List of section variables *)
@@ -1352,8 +1355,7 @@ sig
                                  (* State id on which the completion of type checking is reported *)
                                  const_entry_feedback    : Stateid.t option;
                                  const_entry_type        : Constr.types option;
-                                 const_entry_polymorphic : bool;
-                                 const_entry_universes   : Univ.UContext.t;
+                                 const_entry_universes   : constant_universes_entry;
                                  const_entry_opaque      : bool;
                                  const_entry_inline_code : bool }
   type parameter_entry = Context.Named.t option * bool * Constr.types Univ.in_universe_context * inline
diff --git a/interp/declare.ml b/interp/declare.ml
index 154793a32..f95d025e4 100644
--- a/interp/declare.ml
+++ b/interp/declare.ml
@@ -63,8 +63,12 @@ let cache_variable ((sp,_),o) =
 	impl, true, poly, ctx
     | SectionLocalDef (de) ->
       let univs = Global.push_named_def (id,de) in
+      let poly = match de.const_entry_universes with
+      | Monomorphic_const_entry _ -> false
+      | Polymorphic_const_entry _ -> true
+      in
       Explicit, de.const_entry_opaque,
-      de.const_entry_polymorphic, univs in
+      poly, univs in
   Nametab.push (Nametab.Until 1) (restrict_path 0 sp) (VarRef id);
   add_section_variable id impl poly ctx;
   Dischargedhypsmap.set_discharged_hyps sp [];
@@ -237,22 +241,29 @@ let declare_constant_common id cst =
 
 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 Monomorphic_const_entry univs
+  in
   { const_entry_body = Future.from_val ?fix_exn ((body,Univ.ContextSet.empty), eff);
     const_entry_secctx = None;
     const_entry_type = types;
-    const_entry_polymorphic = poly;
     const_entry_universes = univs;
     const_entry_opaque = opaque;
     const_entry_feedback = None;
     const_entry_inline_code = inline}
 
 let declare_constant ?(internal = UserIndividualRequest) ?(local = false) id ?(export_seff=false) (cd, kind) =
+  let is_poly de = match de.const_entry_universes with
+  | Monomorphic_const_entry _ -> false
+  | Polymorphic_const_entry _ -> true
+  in
   let export = (* We deal with side effects *)
     match cd with
     | DefinitionEntry de when
         export_seff ||
         not de.const_entry_opaque ||
-        de.const_entry_polymorphic ->
+        is_poly de ->
           let bo = de.const_entry_body in
           let _, seff = Future.force bo in
           Safe_typing.empty_private_constants <> seff
diff --git a/kernel/entries.ml b/kernel/entries.ml
index 3fa25c142..a1ccbdbc1 100644
--- a/kernel/entries.ml
+++ b/kernel/entries.ml
@@ -64,6 +64,10 @@ type mutual_inductive_entry = {
 type 'a proof_output = constr Univ.in_universe_context_set * 'a
 type 'a const_entry_body = 'a proof_output Future.computation
 
+type constant_universes_entry =
+  | Monomorphic_const_entry of Univ.universe_context
+  | Polymorphic_const_entry of Univ.universe_context
+
 type 'a definition_entry = {
   const_entry_body   : 'a const_entry_body;
   (* List of section variables *)
@@ -71,8 +75,7 @@ type 'a definition_entry = {
   (* State id on which the completion of type checking is reported *)
   const_entry_feedback : Stateid.t option;
   const_entry_type        : types option;
-  const_entry_polymorphic : bool;
-  const_entry_universes   : Univ.universe_context;
+  const_entry_universes   : constant_universes_entry;
   const_entry_opaque      : bool;
   const_entry_inline_code : bool }
 
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index ed4c7d57a..074122b03 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -382,12 +382,12 @@ let safe_push_named d env =
 
 
 let push_named_def (id,de) senv =
-  let c,typ,univs = 
-    match Term_typing.translate_local_def senv.revstruct senv.env id de with
-    | c, typ, Monomorphic_const ctx -> c, typ, ctx
-    | _, _, Polymorphic_const _ -> assert false
+  let open Entries in
+  let c,typ,univs = Term_typing.translate_local_def senv.revstruct senv.env id de in
+  let poly = match de.Entries.const_entry_universes with
+  | Monomorphic_const_entry _ -> false
+  | Polymorphic_const_entry _ -> true
   in
-  let poly = de.Entries.const_entry_polymorphic in
   let univs = Univ.ContextSet.of_context univs in
   let c, univs = match c with
     | Def c -> Mod_subst.force_constr c, univs
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index cf82d54ec..910223465 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -251,8 +251,8 @@ let infer_declaration ~trust env kn dcl =
       delay even in the polymorphic case.  *)
   | DefinitionEntry ({ const_entry_type = Some typ;
                        const_entry_opaque = true;
-		       const_entry_polymorphic = false} as c) ->
-      let env = push_context ~strict:true c.const_entry_universes env in
+		       const_entry_universes = Monomorphic_const_entry univs } as c) ->
+      let env = push_context ~strict:true univs env in
       let { const_entry_body = body; const_entry_feedback = feedback_id } = c in
       let tyj = infer_type env typ in
       let proofterm =
@@ -271,7 +271,7 @@ let infer_declaration ~trust env kn dcl =
           c, uctx) in
       let def = OpaqueDef (Opaqueproof.create proofterm) in
       def, RegularArity typ, None,
-      (Monomorphic_const c.const_entry_universes),
+      (Monomorphic_const univs),
       c.const_entry_inline_code, c.const_entry_secctx
 
   (** Other definitions have to be processed immediately. *)
@@ -279,18 +279,22 @@ let infer_declaration ~trust env kn dcl =
       let { const_entry_type = typ; const_entry_opaque = opaque } = c in
       let { const_entry_body = body; const_entry_feedback = feedback_id } = c in
       let (body, ctx), side_eff = Future.join body in
-      let univsctx = Univ.ContextSet.of_context c.const_entry_universes in
+      let poly, univs = match c.const_entry_universes with
+      | Monomorphic_const_entry univs -> false, univs
+      | Polymorphic_const_entry univs -> true, univs
+      in
+      let univsctx = Univ.ContextSet.of_context univs in
       let body, ctx, _ = inline_side_effects env body
         (Univ.ContextSet.union univsctx ctx) side_eff in
-      let env = push_context_set ~strict:(not c.const_entry_polymorphic) ctx env in
-      let abstract = c.const_entry_polymorphic && not (Option.is_empty kn) in
+      let env = push_context_set ~strict:(not poly) ctx env in
+      let abstract = poly && not (Option.is_empty kn) in
       let usubst, univs =
         abstract_constant_universes abstract (Univ.ContextSet.to_context ctx)
       in      
       let j = infer env body in
       let typ = match typ with
         | None ->
-           if not c.const_entry_polymorphic then (* Old-style polymorphism *)
+           if not poly then (* Old-style polymorphism *)
              make_polymorphic_if_constant_for_ind env j
            else RegularArity (Vars.subst_univs_level_constr usubst j.uj_type)
         | Some t ->
@@ -461,11 +465,12 @@ let translate_constant mb env kn ce =
     (infer_declaration ~trust:mb env (Some kn) ce)
 
 let constant_entry_of_side_effect cb u =
-  let poly, univs =
+  let univs =
     match cb.const_universes with
-    | Monomorphic_const ctx -> false, ctx
+    | Monomorphic_const uctx ->
+      Monomorphic_const_entry uctx
     | Polymorphic_const auctx -> 
-      true, Univ.AUContext.repr auctx
+      Polymorphic_const_entry (Univ.AUContext.repr auctx)
   in
   let pt =
     match cb.const_body, u with
@@ -478,7 +483,6 @@ let constant_entry_of_side_effect cb u =
     const_entry_feedback = None;
     const_entry_type =
       (match cb.const_type with RegularArity t -> Some t | _ -> None);
-    const_entry_polymorphic = poly;
     const_entry_universes = univs;
     const_entry_opaque = Declareops.is_opaque cb;
     const_entry_inline_code = cb.const_inline_code }
@@ -592,6 +596,10 @@ let translate_local_def mb env id centry =
            env ids_def ids_typ context_ids in
        record_aux env ids_typ ids_def expr
   end;
+  let univs = match univs with
+  | Monomorphic_const ctx -> ctx
+  | Polymorphic_const _ -> assert false
+  in
   def, typ, univs
 
 (* Insertion of inductive types. *)
diff --git a/kernel/term_typing.mli b/kernel/term_typing.mli
index 77d126074..29c991837 100644
--- a/kernel/term_typing.mli
+++ b/kernel/term_typing.mli
@@ -15,7 +15,7 @@ open Entries
 type side_effects
 
 val translate_local_def : structure_body -> env -> Id.t -> side_effects definition_entry ->
-  constant_def * types * constant_universes
+  constant_def * types * Univ.universe_context
 
 val translate_local_assum : env -> types -> types
 
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index 52d6787d4..2ade797f6 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -378,6 +378,10 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now
       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 Entries.Monomorphic_const_entry univs
+      in
 	{ Entries.
 	  const_entry_body = body;
 	  const_entry_secctx = section_vars;
@@ -386,7 +390,7 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now
 	  const_entry_inline_code = false;
 	  const_entry_opaque = true;
 	  const_entry_universes = univs;
-	  const_entry_polymorphic = poly})
+        })
 		fpl initial_goals in
   let binders =
     Option.map (fun names -> fst (Evd.universe_context ~names (Evd.from_ctx universes)))
diff --git a/tactics/ind_tables.ml b/tactics/ind_tables.ml
index 0407c1e36..7f087ea01 100644
--- a/tactics/ind_tables.ml
+++ b/tactics/ind_tables.ml
@@ -123,14 +123,18 @@ let define internal id c p univs =
   let ctx = Evd.normalize_evar_universe_context univs in
   let c = Vars.subst_univs_fn_constr 
     (Universes.make_opt_subst (Evd.evar_universe_context_subst ctx)) c in
+  let univs = Evd.evar_context_universe_context ctx in
+  let univs =
+    if p then Polymorphic_const_entry univs
+    else Monomorphic_const_entry univs
+  in
   let entry = {
     const_entry_body =
       Future.from_val ((c,Univ.ContextSet.empty),
                        Safe_typing.empty_private_constants);
     const_entry_secctx = None;
     const_entry_type = None;
-    const_entry_polymorphic = p;
-    const_entry_universes = Evd.evar_context_universe_context ctx;
+    const_entry_universes = univs;
     const_entry_opaque = false;
     const_entry_inline_code = false;
     const_entry_feedback = None;
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 8a95ad177..cb905e749 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -5004,8 +5004,9 @@ let cache_term_by_tactic_then ~opaque ?(goal_type=None) id gk tac tacK =
   in
   let cst = Impargs.with_implicit_protection cst () in
   let lem =
-    if const.Entries.const_entry_polymorphic then
-      let uctx = Univ.ContextSet.of_context const.Entries.const_entry_universes in
+    match const.Entries.const_entry_universes with
+    | Entries.Polymorphic_const_entry uctx ->
+      let uctx = Univ.ContextSet.of_context uctx in
       (** Hack: the kernel may generate definitions whose universe variables are
           not the same as requested in the entry because of constraints delayed
           in the body, even in polymorphic mode. We mimick what it does for now
@@ -5014,7 +5015,8 @@ let cache_term_by_tactic_then ~opaque ?(goal_type=None) id gk tac tacK =
       let uctx = Univ.ContextSet.to_context (Univ.ContextSet.union uctx body_uctx) in
       let u = Univ.UContext.instance uctx in
       mkConstU (cst, EInstance.make u)
-    else mkConst cst
+    | Entries.Monomorphic_const_entry _ ->
+      mkConst cst
   in
   let evd = Evd.set_universe_context evd ectx in
   let open Safe_typing in
diff --git a/vernac/indschemes.ml b/vernac/indschemes.ml
index 3d97a767c..6ea8bc7f2 100644
--- a/vernac/indschemes.ml
+++ b/vernac/indschemes.ml
@@ -109,13 +109,17 @@ let _ =
 
 let define id internal ctx c t =
   let f = declare_constant ~internal in
+  let _, univs = Evd.universe_context ctx in
+  let univs =
+    if Flags.is_universe_polymorphism () then Polymorphic_const_entry univs
+    else Monomorphic_const_entry univs
+  in
   let kn = f id
     (DefinitionEntry
       { const_entry_body = c;
         const_entry_secctx = None;
         const_entry_type = t;
-	const_entry_polymorphic = Flags.is_universe_polymorphism ();
-	const_entry_universes = snd (Evd.universe_context ctx);
+	const_entry_universes = univs;
         const_entry_opaque = false;
         const_entry_inline_code = false;
         const_entry_feedback = None;
diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index 10d3317f8..02067c190 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -636,12 +636,12 @@ 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_polymorphic = poly;
-	  const_entry_universes = uctx;
+	  const_entry_universes = univs;
 	  const_entry_opaque = opaque;
           const_entry_inline_code = false;
           const_entry_feedback = None;
diff --git a/vernac/record.ml b/vernac/record.ml
index 63ca22786..a2e443e5f 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -322,13 +322,16 @@ 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_polymorphic = poly;
-		    const_entry_universes = ctx;
+		    const_entry_universes = univs;
 		    const_entry_opaque = false;
 		    const_entry_inline_code = false;
 		    const_entry_feedback = None } in