When declaring constants/inductives use ContextSet if monomorphic.

Also use constant_universes_entry instead of a bool flag to indicate
polymorphism in ParameterEntry.

There are a few places where we convert back to ContextSet because
check_univ_decl returns a UContext, this could be improved.

3 files changed, 12 insertions, 7 deletions

diff --git a/printing/prettyp.ml b/printing/prettyp.ml
index 8fc00ed96..b4ac94103 100644
--- a/printing/prettyp.ml
+++ b/printing/prettyp.ml
@@ -556,26 +556,26 @@ let print_constant with_values sep sp =
       Vars.subst_instance_constr inst cb.const_type
   in
   let univs =
+    let open Entries in
     let otab = Global.opaque_tables () in
     match cb.const_body with
     | Undef _ | Def _ ->
       begin
         match cb.const_universes with
-        | Monomorphic_const ctx -> ctx
+        | Monomorphic_const ctx -> Monomorphic_const_entry ctx
         | Polymorphic_const ctx ->
           let inst = Univ.AUContext.instance ctx in
-          Univ.UContext.make (inst, Univ.AUContext.instantiate inst ctx)
+          Polymorphic_const_entry (Univ.UContext.make (inst, Univ.AUContext.instantiate inst ctx))
       end
     | OpaqueDef o ->
       let body_uctxs = Opaqueproof.force_constraints otab o in
       match cb.const_universes with
       | Monomorphic_const ctx ->
-        let uctxs = Univ.ContextSet.of_context ctx in
-        Univ.ContextSet.to_context (Univ.ContextSet.union body_uctxs uctxs)
+        Monomorphic_const_entry (Univ.ContextSet.union body_uctxs ctx)
       | Polymorphic_const ctx ->
         assert(Univ.ContextSet.is_empty body_uctxs);
         let inst = Univ.AUContext.instance ctx in
-        Univ.UContext.make (inst, Univ.AUContext.instantiate inst ctx)
+        Polymorphic_const_entry (Univ.UContext.make (inst, Univ.AUContext.instantiate inst ctx))
   in
   let ctx =
     Evd.evar_universe_context_of_binders
@@ -589,12 +589,12 @@ let print_constant with_values sep sp =
 	str"*** [ " ++
 	print_basename sp ++ print_instance sigma cb ++ str " : " ++ cut () ++ pr_ltype typ ++
 	str" ]" ++
-	Printer.pr_universe_ctx sigma univs
+        Printer.pr_constant_universes sigma univs
     | Some (c, ctx) ->
         let c = Vars.subst_instance_constr (Univ.AUContext.instance ctx) c in
 	print_basename sp ++ print_instance sigma cb ++ str sep ++ cut () ++
 	(if with_values then print_typed_body env sigma (Some c,typ) else pr_ltype typ)++
-        Printer.pr_universe_ctx sigma univs)
+        Printer.pr_constant_universes sigma univs)
 
 let gallina_print_constant_with_infos sp =
   print_constant true " = " sp ++
diff --git a/printing/printer.ml b/printing/printer.ml
index 4d5cfcba3..ae6292024 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -270,6 +270,10 @@ let pr_universe_ctx sigma c =
   else
     mt()
 
+let pr_constant_universes sigma = function
+  | Entries.Monomorphic_const_entry ctx -> pr_universe_ctx_set sigma ctx
+  | Entries.Polymorphic_const_entry ctx -> pr_universe_ctx sigma ctx
+
 let pr_cumulativity_info sigma cumi =
   if !Detyping.print_universes 
   && not (Univ.UContext.is_empty (Univ.CumulativityInfo.univ_context cumi)) then
diff --git a/printing/printer.mli b/printing/printer.mli
index a3d0eaac2..67128da40 100644
--- a/printing/printer.mli
+++ b/printing/printer.mli
@@ -122,6 +122,7 @@ val pr_cumulative          : bool -> bool -> Pp.t
 val pr_universe_instance   : evar_map -> Univ.UContext.t -> Pp.t
 val pr_universe_ctx        : evar_map -> Univ.UContext.t -> Pp.t
 val pr_universe_ctx_set    : evar_map -> Univ.ContextSet.t -> Pp.t
+val pr_constant_universes  : evar_map -> Entries.constant_universes_entry -> Pp.t
 val pr_cumulativity_info   : evar_map -> Univ.CumulativityInfo.t -> Pp.t
 
 (** Printing global references using names as short as possible *)