From a5feb9687819c5e7ef0db6e7b74d0e236a296674 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
Date: Fri, 15 Sep 2017 21:01:57 +0200
Subject: Separate checking univ_decls and obtaining universe binder names.

---
 printing/printer.ml  | 7 +++++++
 printing/printer.mli | 1 +
 2 files changed, 8 insertions(+)

(limited to 'printing')

diff --git a/printing/printer.ml b/printing/printer.ml
index d7bb0460d..4d5cfcba3 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -256,6 +256,13 @@ let safe_pr_constr t =
   let (sigma, env) = Pfedit.get_current_context () in
   safe_pr_constr_env env sigma t
 
+let pr_universe_ctx_set sigma c =
+  if !Detyping.print_universes && not (Univ.ContextSet.is_empty c) then
+    fnl()++pr_in_comment (fun c -> v 0
+      (Univ.pr_universe_context_set (Termops.pr_evd_level sigma) c)) c
+  else
+    mt()
+
 let pr_universe_ctx sigma c =
   if !Detyping.print_universes && not (Univ.UContext.is_empty c) then
     fnl()++pr_in_comment (fun c -> v 0 
diff --git a/printing/printer.mli b/printing/printer.mli
index e014baa2c..a3d0eaac2 100644
--- a/printing/printer.mli
+++ b/printing/printer.mli
@@ -121,6 +121,7 @@ val pr_polymorphic         : bool -> Pp.t
 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_cumulativity_info   : evar_map -> Univ.CumulativityInfo.t -> Pp.t
 
 (** Printing global references using names as short as possible *)
-- 
cgit v1.2.3


From 58c0784745f8b2ba7523f246c4611d780c9f3f70 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
Date: Mon, 18 Sep 2017 14:50:07 +0200
Subject: 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.
---
 API/API.mli                       | 11 +++++-----
 checker/cic.mli                   |  4 ++--
 checker/mod_checking.ml           |  2 +-
 checker/values.ml                 |  6 ++---
 interp/declare.ml                 |  6 +++--
 kernel/declarations.ml            |  6 ++---
 kernel/declareops.ml              |  4 ++--
 kernel/entries.ml                 | 10 +++++----
 kernel/indtypes.ml                |  9 ++++----
 kernel/mod_typing.ml              | 26 ++++++++++++----------
 kernel/safe_typing.ml             | 12 +++++-----
 kernel/term_typing.ml             | 46 ++++++++++++++++++++++-----------------
 kernel/term_typing.mli            |  2 +-
 kernel/univ.ml                    |  1 +
 kernel/univ.mli                   |  5 ++++-
 kernel/vconv.ml                   |  2 +-
 plugins/ltac/rewrite.ml           |  6 ++++-
 printing/prettyp.ml               | 14 ++++++------
 printing/printer.ml               |  4 ++++
 printing/printer.mli              |  1 +
 proofs/proof_global.ml            | 12 +++++-----
 tactics/ind_tables.ml             |  5 ++---
 test-suite/output/UnivBinders.out |  2 +-
 vernac/classes.ml                 | 34 +++++++++++++++++++----------
 vernac/command.ml                 | 15 ++++++++-----
 vernac/indschemes.ml              |  6 ++---
 vernac/lemmas.ml                  | 19 ++++++++++++----
 vernac/obligations.ml             | 45 ++++++++++++++++++++++----------------
 vernac/record.ml                  | 36 +++++++++++++++---------------
 29 files changed, 205 insertions(+), 146 deletions(-)

(limited to 'printing')

diff --git a/API/API.mli b/API/API.mli
index 5c7860671..ad5d5490b 100644
--- a/API/API.mli
+++ b/API/API.mli
@@ -1417,7 +1417,7 @@ sig
     | TemplateArity of 'b
 
   type constant_universes =
-    | Monomorphic_const of Univ.UContext.t
+    | Monomorphic_const of Univ.ContextSet.t
     | Polymorphic_const of Univ.AUContext.t
 
   type projection_body = {
@@ -1484,7 +1484,7 @@ sig
                        | MEwith of module_alg_expr * with_declaration
 
   type abstract_inductive_universes =
-  | Monomorphic_ind of Univ.UContext.t
+  | Monomorphic_ind of Univ.ContextSet.t
   | Polymorphic_ind of Univ.AUContext.t
   | Cumulative_ind of Univ.ACumulativityInfo.t
 
@@ -1551,7 +1551,7 @@ sig
     | LocalAssumEntry of constr
 
   type inductive_universes =
-    | Monomorphic_ind_entry of Univ.UContext.t
+    | Monomorphic_ind_entry of Univ.ContextSet.t
     | Polymorphic_ind_entry of Univ.UContext.t
     | Cumulative_ind_entry of Univ.CumulativityInfo.t
 
@@ -1580,8 +1580,9 @@ sig
   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.UContext.t
+    | Monomorphic_const_entry of Univ.ContextSet.t
     | Polymorphic_const_entry of Univ.UContext.t
+  type 'a in_constant_universes_entry = 'a * constant_universes_entry
   type 'a definition_entry =
                                { const_entry_body   : 'a const_entry_body;
                                  (* List of section variables *)
@@ -1592,7 +1593,7 @@ sig
                                  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
+  type parameter_entry = Context.Named.t option * Constr.types in_constant_universes_entry * inline
 
   type projection_entry = {
     proj_entry_ind : MutInd.t;
diff --git a/checker/cic.mli b/checker/cic.mli
index 354650964..4a0e706aa 100644
--- a/checker/cic.mli
+++ b/checker/cic.mli
@@ -208,7 +208,7 @@ type constant_def =
   | OpaqueDef of lazy_constr
 
 type constant_universes =
-  | Monomorphic_const of Univ.universe_context
+  | Monomorphic_const of Univ.ContextSet.t
   | Polymorphic_const of Univ.abstract_universe_context
 
 (** The [typing_flags] are instructions to the type-checker which
@@ -303,7 +303,7 @@ type one_inductive_body = {
   }
 
 type abstract_inductive_universes =
-  | Monomorphic_ind of Univ.universe_context
+  | Monomorphic_ind of Univ.ContextSet.t
   | Polymorphic_ind of Univ.abstract_universe_context
   | Cumulative_ind of Univ.abstract_cumulativity_info
 
diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml
index 63e28448f..4357a690e 100644
--- a/checker/mod_checking.ml
+++ b/checker/mod_checking.ml
@@ -29,7 +29,7 @@ let check_constant_declaration env kn cb =
   (** [env'] contains De Bruijn universe variables *)
   let env' =
     match cb.const_universes with
-    | Monomorphic_const ctx -> push_context ~strict:true ctx env
+    | Monomorphic_const ctx -> push_context_set ~strict:true ctx env
     | Polymorphic_const auctx ->
       let ctx = Univ.AUContext.repr auctx in
       push_context ~strict:false ctx env
diff --git a/checker/values.ml b/checker/values.ml
index 9e16c8435..5a371164c 100644
--- a/checker/values.ml
+++ b/checker/values.ml
@@ -13,7 +13,7 @@
 To ensure this file is up-to-date, 'make' now compares the md5 of cic.mli
 with a copy we maintain here:
 
-MD5 f4b00c567a972ae950b9ed10c533fda5 checker/cic.mli
+MD5 56ac4cade33eff3d26ed5cdadb580c7e checker/cic.mli
 
 *)
 
@@ -215,7 +215,7 @@ let v_projbody =
 let v_typing_flags =
   v_tuple "typing_flags" [|v_bool; v_bool|]
 
-let v_const_univs = v_sum "constant_universes" 0 [|[|v_context|]; [|v_abs_context|]|]
+let v_const_univs = v_sum "constant_universes" 0 [|[|v_context_set|]; [|v_abs_context|]|]
 
 let v_cb = v_tuple "constant_body"
   [|v_section_ctxt;
@@ -265,7 +265,7 @@ let v_mind_record = Annot ("mind_record",
 
 let v_ind_pack_univs = 
   v_sum "abstract_inductive_universes" 0
-    [|[|v_context|]; [|v_abs_context|]; [|v_abs_cum_info|]|]
+    [|[|v_context_set|]; [|v_abs_context|]; [|v_abs_cum_info|]|]
 
 let v_ind_pack = v_tuple "mutual_inductive_body"
   [|Array v_one_ind;
diff --git a/interp/declare.ml b/interp/declare.ml
index dc77981f2..15999f1d1 100644
--- a/interp/declare.ml
+++ b/interp/declare.ml
@@ -207,7 +207,9 @@ 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
+    else
+      (* FIXME be smarter about this *)
+      Monomorphic_const_entry (Univ.ContextSet.of_context univs)
   in
   { const_entry_body = Future.from_val ?fix_exn ((body,Univ.ContextSet.empty), eff);
     const_entry_secctx = None;
@@ -340,7 +342,7 @@ let dummy_inductive_entry (_,m) = ([],{
   mind_entry_record = None;
   mind_entry_finite = Decl_kinds.BiFinite;
   mind_entry_inds = List.map dummy_one_inductive_entry m.mind_entry_inds;
-  mind_entry_universes = Monomorphic_ind_entry Univ.UContext.empty;
+  mind_entry_universes = Monomorphic_ind_entry Univ.ContextSet.empty;
   mind_entry_private = None;
 })
 
diff --git a/kernel/declarations.ml b/kernel/declarations.ml
index b95796fd8..d5312c500 100644
--- a/kernel/declarations.ml
+++ b/kernel/declarations.ml
@@ -63,7 +63,7 @@ type constant_def =
   | OpaqueDef of Opaqueproof.opaque       (** or an opaque global definition *)
 
 type constant_universes =
-  | Monomorphic_const of Univ.UContext.t
+  | Monomorphic_const of Univ.ContextSet.t
   | Polymorphic_const of Univ.AUContext.t
 
 (** The [typing_flags] are instructions to the type-checker which
@@ -168,9 +168,9 @@ type one_inductive_body = {
   }
 
 type abstract_inductive_universes =
-  | Monomorphic_ind of Univ.UContext.t
+  | Monomorphic_ind of Univ.ContextSet.t
   | Polymorphic_ind of Univ.AUContext.t
-  | Cumulative_ind  of Univ.ACumulativityInfo.t
+  | Cumulative_ind of Univ.ACumulativityInfo.t
 
 type mutual_inductive_body = {
 
diff --git a/kernel/declareops.ml b/kernel/declareops.ml
index f5c26b33d..d8768a0fc 100644
--- a/kernel/declareops.ml
+++ b/kernel/declareops.ml
@@ -126,7 +126,7 @@ let hcons_const_def = function
 let hcons_const_universes cbu =
   match cbu with
   | Monomorphic_const ctx -> 
-    Monomorphic_const (Univ.hcons_universe_context ctx)
+    Monomorphic_const (Univ.hcons_universe_context_set ctx)
   | Polymorphic_const ctx -> 
     Polymorphic_const (Univ.hcons_abstract_universe_context ctx)
 
@@ -274,7 +274,7 @@ let hcons_mind_packet oib =
 
 let hcons_mind_universes miu =
   match miu with
-  | Monomorphic_ind ctx -> Monomorphic_ind (Univ.hcons_universe_context ctx)
+  | Monomorphic_ind ctx -> Monomorphic_ind (Univ.hcons_universe_context_set ctx)
   | Polymorphic_ind ctx -> Polymorphic_ind (Univ.hcons_abstract_universe_context ctx)
   | Cumulative_ind cui -> Cumulative_ind (Univ.hcons_abstract_cumulativity_info cui)
 
diff --git a/kernel/entries.ml b/kernel/entries.ml
index 185dba409..c44a17df2 100644
--- a/kernel/entries.ml
+++ b/kernel/entries.ml
@@ -35,9 +35,9 @@ then, in i{^ th} block, [mind_entry_params] is [xn:Xn;...;x1:X1];
 *)
 
 type inductive_universes =
-  | Monomorphic_ind_entry of Univ.UContext.t
+  | Monomorphic_ind_entry of Univ.ContextSet.t
   | Polymorphic_ind_entry of Univ.UContext.t
-  | Cumulative_ind_entry  of Univ.CumulativityInfo.t
+  | Cumulative_ind_entry of Univ.CumulativityInfo.t
 
 type one_inductive_entry = {
   mind_entry_typename : Id.t;
@@ -65,9 +65,11 @@ 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.UContext.t
+  | Monomorphic_const_entry of Univ.ContextSet.t
   | Polymorphic_const_entry of Univ.UContext.t
 
+type 'a in_constant_universes_entry = 'a * constant_universes_entry
+
 type 'a definition_entry = {
   const_entry_body   : 'a const_entry_body;
   (* List of section variables *)
@@ -82,7 +84,7 @@ type 'a definition_entry = {
 type inline = int option (* inlining level, None for no inlining *)
 
 type parameter_entry = 
-    Context.Named.t option * bool * types Univ.in_universe_context * inline 
+    Context.Named.t option * types in_constant_universes_entry * inline
 
 type projection_entry = {
   proj_entry_ind : MutInd.t;
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 083b0ae40..8e9b606a5 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -265,13 +265,12 @@ let typecheck_inductive env mie =
   (* Check unicity of names *)
   mind_check_names mie;
   (* Params are typed-checked here *)
-  let univctx =
+  let env' =
     match mie.mind_entry_universes with
-    | Monomorphic_ind_entry ctx -> ctx
-    | Polymorphic_ind_entry ctx -> ctx
-    | Cumulative_ind_entry cumi -> Univ.CumulativityInfo.univ_context cumi
+    | Monomorphic_ind_entry ctx -> push_context_set ctx env
+    | Polymorphic_ind_entry ctx -> push_context ctx env
+    | Cumulative_ind_entry cumi -> push_context (Univ.CumulativityInfo.univ_context cumi) env
   in
-  let env' = push_context univctx env in
   let (env_params,paramsctxt) = infer_local_decls env' mie.mind_entry_params in
   (* We first type arity of each inductive definition *)
   (* This allows building the environment of arities and to share *)
diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml
index 8568bf14b..f7e755f00 100644
--- a/kernel/mod_typing.ml
+++ b/kernel/mod_typing.ml
@@ -79,18 +79,20 @@ let rec check_with_def env struc (idl,(c,ctx)) mp equiv =
               environment, because they do not appear in the type of the
               definition. Any inconsistency will be raised at a later stage
               when joining the environment. *)
-	  let env' = Environ.push_context ~strict:true ctx env' in
-	  let c',cst = match cb.const_body with
-	    | Undef _ | OpaqueDef _ ->
-	      let j = Typeops.infer env' c in
-	      let typ = cb.const_type in
-	      let cst' = Reduction.infer_conv_leq env' (Environ.universes env')
-						j.uj_type typ in
-	      j.uj_val, cst'
-	    | Def cs ->
-	       let c' = Mod_subst.force_constr cs in
-	         c, Reduction.infer_conv env' (Environ.universes env') c c'
-	  in c', Monomorphic_const ctx, Univ.ContextSet.add_constraints cst (Univ.ContextSet.of_context ctx)
+          let env' = Environ.push_context ~strict:true ctx env' in
+          let c',cst = match cb.const_body with
+            | Undef _ | OpaqueDef _ ->
+              let j = Typeops.infer env' c in
+              let typ = cb.const_type in
+              let cst' = Reduction.infer_conv_leq env' (Environ.universes env')
+                  j.uj_type typ in
+              j.uj_val, cst'
+            | Def cs ->
+              let c' = Mod_subst.force_constr cs in
+              c, Reduction.infer_conv env' (Environ.universes env') c c'
+          in
+          let ctx = Univ.ContextSet.of_context ctx in
+          c', Monomorphic_const ctx, Univ.ContextSet.add_constraints cst ctx
         | Polymorphic_const uctx ->
           let subst, ctx = Univ.abstract_universes ctx in
           let c = Vars.subst_univs_level_constr subst c in
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 0e416b3e5..0e41bfc3c 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -249,14 +249,14 @@ let universes_of_private eff =
               in
               match cb.const_universes with
               | Monomorphic_const ctx ->
-                (Univ.ContextSet.of_context ctx) :: acc
+                ctx :: acc
               | Polymorphic_const _ -> acc
            )
            acc l
        | Entries.SEsubproof (c, cb, e) ->
          match cb.const_universes with
               | Monomorphic_const ctx ->
-                (Univ.ContextSet.of_context ctx) :: acc
+                ctx :: acc
               | Polymorphic_const _ -> acc
     )
     [] (Term_typing.uniq_seff eff)
@@ -389,7 +389,6 @@ let push_named_def (id,de) senv =
   | Monomorphic_const_entry _ -> false
   | Polymorphic_const_entry _ -> true
   in
-  let univs = Univ.ContextSet.of_context univs in
   let c, univs = match c with
     | Def c -> Mod_subst.force_constr c, univs
     | OpaqueDef o ->
@@ -425,9 +424,8 @@ let labels_of_mib mib =
 
 let globalize_constant_universes env cb =
   match cb.const_universes with
-  | Monomorphic_const ctx ->
-    let cstrs = Univ.ContextSet.of_context ctx in
-    Now (false, cstrs) ::  
+  | Monomorphic_const cstrs ->
+    Now (false, cstrs) ::
     (match cb.const_body with
      | (Undef _ | Def _) -> []
      | OpaqueDef lc ->
@@ -443,7 +441,7 @@ let globalize_constant_universes env cb =
 let globalize_mind_universes mb =
   match mb.mind_universes with
   | Monomorphic_ind ctx ->
-    [Now (false, Univ.ContextSet.of_context ctx)]
+    [Now (false, ctx)]
   | Polymorphic_ind _ -> [Now (true, Univ.ContextSet.empty)]
   | Cumulative_ind _ -> [Now (true, Univ.ContextSet.empty)]
 
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index 4617f2d5f..70dd6438d 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -125,11 +125,10 @@ let inline_side_effects env body ctx side_eff =
       | _ -> assert false
       in
       match cb.const_universes with
-      | Monomorphic_const cnstctx ->
+      | Monomorphic_const univs ->
         (** Abstract over the term at the top of the proof *)
         let ty = cb.const_type in
         let subst = Cmap_env.add c (Inr var) subst in
-        let univs = Univ.ContextSet.of_context cnstctx in
         let ctx = Univ.ContextSet.union ctx univs in
         (subst, var + 1, ctx, (cname c, b, ty, opaque) :: args)
       | Polymorphic_const auctx ->
@@ -228,19 +227,25 @@ let feedback_completion_typecheck =
   Option.iter (fun state_id ->
       feedback ~id:state_id Feedback.Complete)
 
-let abstract_constant_universes abstract uctx =
-  if not abstract then
+let abstract_constant_universes abstract = function
+  | Monomorphic_const_entry uctx ->
     Univ.empty_level_subst, Monomorphic_const uctx
-  else
-    let sbst, auctx = Univ.abstract_universes uctx in
-    sbst, Polymorphic_const auctx
+  | Polymorphic_const_entry uctx ->
+    if not abstract then
+      Univ.empty_level_subst, Monomorphic_const (Univ.ContextSet.of_context uctx)
+    else
+      let sbst, auctx = Univ.abstract_universes uctx in
+      sbst, Polymorphic_const auctx
 
 let infer_declaration (type a) ~(trust : a trust) env kn (dcl : a constant_entry) =
   match dcl with
-  | ParameterEntry (ctx,poly,(t,uctx),nl) ->
-      let env = push_context ~strict:(not poly) uctx env in
+    | ParameterEntry (ctx,(t,uctx),nl) ->
+      let env = match uctx with
+        | Monomorphic_const_entry uctx -> push_context_set ~strict:true uctx env
+        | Polymorphic_const_entry uctx -> push_context ~strict:false uctx env
+      in
       let j = infer env t in
-      let abstract = poly && not (Option.is_empty kn) in
+      let abstract = not (Option.is_empty kn) in
       let usubst, univs = 
         abstract_constant_universes abstract uctx
       in
@@ -262,7 +267,7 @@ let infer_declaration (type a) ~(trust : a trust) env kn (dcl : a constant_entry
   | DefinitionEntry ({ const_entry_type = Some typ;
                        const_entry_opaque = true;
 		       const_entry_universes = Monomorphic_const_entry univs } as c) ->
-      let env = push_context ~strict:true univs env in
+      let env = push_context_set ~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 =
@@ -301,21 +306,22 @@ let infer_declaration (type a) ~(trust : a trust) env kn (dcl : a constant_entry
       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 poly, univs = match c.const_entry_universes with
+      let poly, univsctx = match c.const_entry_universes with
       | Monomorphic_const_entry univs -> false, univs
-      | Polymorphic_const_entry univs -> true, univs
+      | Polymorphic_const_entry univs -> true, Univ.ContextSet.of_context univs
       in
-      let univsctx = Univ.ContextSet.of_context univs in
       let ctx = Univ.ContextSet.union univsctx ctx in
       let body, ctx, _ = match trust with
       | Pure -> body, ctx, []
       | SideEffects _ -> inline_side_effects env body ctx side_eff
       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 abstract = not (Option.is_empty kn) in
+      let ctx = if poly
+        then Polymorphic_const_entry (Univ.ContextSet.to_context ctx)
+        else Monomorphic_const_entry ctx
+      in
+      let usubst, univs = abstract_constant_universes abstract ctx in
       let j = infer env body in
       let typ = match typ with
         | None ->
@@ -556,7 +562,7 @@ let export_side_effects mb env ce =
             let env = Environ.add_constant kn cb env in
             match cb.const_universes with
             | Monomorphic_const ctx ->
-              Environ.push_context ~strict:true ctx env
+              Environ.push_context_set ~strict:true ctx env
             | Polymorphic_const _ -> env
           end
         | kn, cb, `Opaque(_, ctx), _ ->
@@ -564,7 +570,7 @@ let export_side_effects mb env ce =
             let env = Environ.add_constant kn cb env in
             match cb.const_universes with
             | Monomorphic_const cstctx ->
-              let env = Environ.push_context ~strict:true cstctx env in
+              let env = Environ.push_context_set ~strict:true cstctx env in
               Environ.push_context_set ~strict:true ctx env
             | Polymorphic_const _ -> env
           end
diff --git a/kernel/term_typing.mli b/kernel/term_typing.mli
index 9b35bfc6e..55da4197e 100644
--- a/kernel/term_typing.mli
+++ b/kernel/term_typing.mli
@@ -19,7 +19,7 @@ type _ trust =
 | SideEffects : structure_body -> side_effects trust
 
 val translate_local_def : 'a trust -> env -> Id.t -> 'a definition_entry ->
-  constant_def * types * Univ.UContext.t
+  constant_def * types * Univ.ContextSet.t
 
 val translate_local_assum : env -> types -> types
 
diff --git a/kernel/univ.ml b/kernel/univ.ml
index 7fe4f8274..64afb95d5 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -1053,6 +1053,7 @@ struct
   let constraints (univs, cst) = cst
   let levels (univs, cst) = univs
 
+  let size (univs,_) = LSet.cardinal univs
 end
 
 type universe_context_set = ContextSet.t
diff --git a/kernel/univ.mli b/kernel/univ.mli
index 8d46a8bee..c06ce2446 100644
--- a/kernel/univ.mli
+++ b/kernel/univ.mli
@@ -310,7 +310,7 @@ sig
   (** Keeps the order of the instances *)
   val union : t -> t -> t
 
-  (* the number of universes in the context *)
+  (** the number of universes in the context *)
   val size : t -> int
 
 end
@@ -423,6 +423,9 @@ sig
 
   val constraints : t -> constraints
   val levels : t -> LSet.t
+
+  (** the number of universes in the context *)
+  val size : t -> int
 end
 
 (** A set of universes with universe constraints.
diff --git a/kernel/vconv.ml b/kernel/vconv.ml
index 0e452621c..578a89371 100644
--- a/kernel/vconv.ml
+++ b/kernel/vconv.ml
@@ -93,7 +93,7 @@ and conv_atom env pb k a1 stk1 a2 stk2 cu =
         let mib = Environ.lookup_mind mi env in
 	let ulen = 
           match mib.Declarations.mind_universes with
-          | Declarations.Monomorphic_ind ctx -> Univ.UContext.size ctx
+          | Declarations.Monomorphic_ind ctx -> Univ.ContextSet.size ctx
           | Declarations.Polymorphic_ind auctx -> Univ.AUContext.size auctx
           | Declarations.Cumulative_ind cumi -> 
             Univ.AUContext.size (Univ.ACumulativityInfo.univ_context cumi)
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index f6523d28c..a2f5a4577 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -1972,9 +1972,13 @@ 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 cst = Declare.declare_constant ~internal:Declare.InternalTacticRequest instance_id
 				(Entries.ParameterEntry 
-				 (None,poly,(instance,UState.context uctx),None),
+                                 (None,(instance,uctx),None),
 				 Decl_kinds.IsAssumption Decl_kinds.Logical)
       in
 	add_instance (Typeclasses.new_instance 
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 *)
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index ea0408169..905173efc 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -331,7 +331,7 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now
   let initial_euctx = Proof.initial_euctx proof in
   let fpl, univs = Future.split2 fpl in
   let universes = if poly || now then Future.force univs else initial_euctx in
-  let univctx = Evd.check_univ_decl (Evd.from_ctx universes) universe_decl in
+  let univctx = UState.check_univ_decl 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
@@ -360,7 +360,7 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now
              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 = Evd.check_univ_decl (Evd.from_ctx ctx_body) universe_decl in
+          let univs = UState.check_univ_decl ctx_body universe_decl in
           (initunivs, typ), ((body, Univ.ContextSet.of_context univs), eff)
         else
           (* Since the proof is computed now, we can simply have 1 set of
@@ -370,7 +370,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 = Evd.check_univ_decl (Evd.from_ctx ctx) universe_decl in
+          let univs = UState.check_univ_decl ctx universe_decl in
           (univs, typ), ((body, Univ.ContextSet.empty), eff)
       in 
        fun t p -> Future.split2 (Future.chain p (make_body t))
@@ -383,7 +383,7 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now
              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 = Evd.check_univ_decl (Evd.from_ctx bodyunivs) universe_decl in
+          let univs = UState.check_univ_decl bodyunivs universe_decl in
           (pt,Univ.ContextSet.of_context univs),eff)
   in
   let entry_fn p (_, t) =
@@ -392,7 +392,9 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now
     let univs, typ = Future.force univstyp in
     let univs =
       if poly then Entries.Polymorphic_const_entry univs
-      else Entries.Monomorphic_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;
diff --git a/tactics/ind_tables.ml b/tactics/ind_tables.ml
index 92c326b1e..e1bf32f3c 100644
--- a/tactics/ind_tables.ml
+++ b/tactics/ind_tables.ml
@@ -123,10 +123,9 @@ 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 = UState.context ctx in
   let univs =
-    if p then Polymorphic_const_entry univs
-    else Monomorphic_const_entry univs
+    if p then Polymorphic_const_entry (UState.context ctx)
+    else Monomorphic_const_entry (UState.context_set ctx)
   in
   let entry = {
     const_entry_body =
diff --git a/test-suite/output/UnivBinders.out b/test-suite/output/UnivBinders.out
index 1bacb7513..42fb52a3b 100644
--- a/test-suite/output/UnivBinders.out
+++ b/test-suite/output/UnivBinders.out
@@ -50,6 +50,6 @@ Type@{Top.17} -> Type@{v} -> Type@{u}
 foo is universe polymorphic
 Monomorphic mono = Type@{u}
      : Type@{u+1}
-(* u |=  *)
+(* {u} |=  *)
 
 mono is not universe polymorphic
diff --git a/vernac/classes.ml b/vernac/classes.ml
index 6f5f96ee2..c99eba2cc 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -200,16 +200,22 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance)
 	let nf, subst = Evarutil.e_nf_evars_and_universes evars in
 	let termtype =
 	  let t = it_mkProd_or_LetIn ty_constr (ctx' @ ctx) in
-	    nf t
-	in
-	Pretyping.check_evars env Evd.empty !evars (EConstr.of_constr termtype);
+            nf t
+        in
+        Pretyping.check_evars env Evd.empty !evars (EConstr.of_constr termtype);
         let ctx = Evd.check_univ_decl !evars decl in
-	let cst = Declare.declare_constant ~internal:Declare.InternalTacticRequest id
-	  (ParameterEntry 
-            (None,poly,(termtype,ctx),None), Decl_kinds.IsAssumption Decl_kinds.Logical)
-	in
+        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 cst = Declare.declare_constant ~internal:Declare.InternalTacticRequest id
+          (ParameterEntry
+            (None,(termtype,ctx),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
+          instance_hook k pri global imps ?hook (ConstRef cst); id
       end
     else (
       let props =
@@ -384,14 +390,20 @@ let context poly l =
   let uctx = ref (Evd.universe_context_set !evars) in
   let fn status (id, b, t) =
     if Lib.is_modtype () && not (Lib.sections_are_opened ()) then
-      let ctx = Univ.ContextSet.to_context !uctx in
       (* Declare the universe context once *)
+      let univs = !uctx in
       let () = uctx := Univ.ContextSet.empty in
       let decl = match b with
       | None ->
-        (ParameterEntry (None,poly,(t,ctx),None), IsAssumption Logical)
+        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 ->
-        let entry = Declare.definition_entry ~poly ~univs:ctx ~types:t b in
+        (* FIXME be smarter about this *)
+        let univs = Univ.ContextSet.to_context univs in
+        let entry = Declare.definition_entry ~poly ~univs ~types:t b in
         (DefinitionEntry entry, IsAssumption Logical)
       in
       let cst = Declare.declare_constant ~internal:Declare.InternalTacticRequest id decl in
diff --git a/vernac/command.ml b/vernac/command.ml
index 80599c534..06d0c8470 100644
--- a/vernac/command.ml
+++ b/vernac/command.ml
@@ -197,8 +197,11 @@ match local with
     | DefaultInline -> Some (Flags.get_inline_level())
     | InlineAt i -> Some i
   in
-  let ctx = Univ.ContextSet.to_context ctx in
-  let decl = (ParameterEntry (None,p,(c,ctx),inl), IsAssumption kind) in
+  let ctx = if p
+    then Polymorphic_const_entry (Univ.ContextSet.to_context ctx)
+    else Monomorphic_const_entry ctx
+  in
+  let decl = (ParameterEntry (None,(c,ctx),inl), IsAssumption kind) in
   let kn = declare_constant ident ~local decl in
   let gr = ConstRef kn in
   let () = maybe_declare_manual_implicits false gr imps in
@@ -206,9 +209,9 @@ match local with
   let () = assumption_message ident in
   let () = Typeclasses.declare_instance None false gr in
   let () = if is_coe then Class.try_add_new_coercion gr ~local p in
-  let inst = 
-    if p (* polymorphic *) then Univ.UContext.instance ctx 
-    else Univ.Instance.empty
+  let inst = match ctx with
+    | Polymorphic_const_entry ctx -> Univ.UContext.instance ctx
+    | Monomorphic_const_entry _ -> Univ.Instance.empty
   in
     (gr,inst,Lib.is_modtype_strict ())
 
@@ -606,7 +609,7 @@ let interp_mutual_inductive (paramsl,indl) notations cum poly prv finite =
         Cumulative_ind_entry (Universes.univ_inf_ind_from_universe_context uctx)
       else Polymorphic_ind_entry uctx
     else
-      Monomorphic_ind_entry uctx
+      Monomorphic_ind_entry (Univ.ContextSet.of_context uctx)
   in
   (* Build the mutual inductive entry *)
   let mind_ent =
diff --git a/vernac/indschemes.ml b/vernac/indschemes.ml
index c728c2671..e4ca98749 100644
--- a/vernac/indschemes.ml
+++ b/vernac/indschemes.ml
@@ -109,10 +109,10 @@ let _ =
 
 let define id internal ctx c t =
   let f = declare_constant ~internal in
-  let univs = Evd.to_universe_context ctx in
   let univs =
-    if Flags.is_universe_polymorphism () then Polymorphic_const_entry univs
-    else Monomorphic_const_entry univs
+    if Flags.is_universe_polymorphism ()
+    then Polymorphic_const_entry (Evd.to_universe_context ctx)
+    else Monomorphic_const_entry (Evd.universe_context_set ctx)
   in
   let kn = f id
     (DefinitionEntry
diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index 71d80c4db..f59b5fcae 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -242,7 +242,11 @@ let save_remaining_recthms (locality,p,kind) norm ctx body opaq i (id,(t_i,(_,im
           | Global -> false
           | Discharge -> assert false
           in
-          let decl = (ParameterEntry (None,p,(t_i,ctx),None), k) 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 kn = declare_constant id ~local decl in
           (locality,ConstRef kn,imps))
   | Some body ->
@@ -491,9 +495,12 @@ 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 = UState.context (fst universes) 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 sec_vars = if !keep_admitted_vars then const_entry_secctx else None in
-            Admitted(id, k, (sec_vars, pi2 k, (typ, ctx), None), universes)
+            Admitted(id, k, (sec_vars, (typ, ctx), None), universes)
         | None ->
             let pftree = Proof_global.give_me_the_proof () in
             let id, k, typ = Pfedit.current_proof_statement () in
@@ -516,8 +523,12 @@ let save_proof ?proof = function
             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 binders = if poly then Some (UState.universe_binders universes) else None in
-            Admitted(id,k,(sec_vars, poly, (typ, ctx), None),
+            Admitted(id,k,(sec_vars, (typ, ctx), None),
 		     (universes, binders))
       in
       Proof_global.apply_terminator (Proof_global.get_terminator ()) pe
diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index 43af8968f..a9110c76c 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -633,12 +633,11 @@ let declare_obligation prg obl body ty uctx =
 	  shrink_body body ty else [], body, ty, [||]
       in
       let body = ((body,Univ.ContextSet.empty),Safe_typing.empty_private_constants) in
-      let univs = if poly then Polymorphic_const_entry uctx else Monomorphic_const_entry uctx in
       let ce =
         { const_entry_body = Future.from_val ~fix_exn:(fun x -> x) body;
           const_entry_secctx = None;
 	  const_entry_type = ty;
-	  const_entry_universes = univs;
+          const_entry_universes = uctx;
 	  const_entry_opaque = opaque;
           const_entry_inline_code = false;
           const_entry_feedback = None;
@@ -647,13 +646,15 @@ let declare_obligation prg obl body ty uctx =
       let constant = Declare.declare_constant obl.obl_name ~local:true
 	(DefinitionEntry ce,IsProof Property)
       in
-	if not opaque then add_hint (Locality.make_section_locality None) prg constant;
-	definition_message obl.obl_name;
-	true, { obl with obl_body =
-	    if poly then
-	      Some (DefinedObl (constant, Univ.UContext.instance uctx))
-	    else
-	      Some (TermObl (it_mkLambda_or_LetIn_or_clean (mkApp (mkConst constant, args)) ctx)) }
+      if not opaque then add_hint (Locality.make_section_locality None) prg constant;
+      definition_message obl.obl_name;
+      let body = match uctx with
+        | Polymorphic_const_entry uctx ->
+          Some (DefinedObl (constant, Univ.UContext.instance uctx))
+        | Monomorphic_const_entry _ ->
+          Some (TermObl (it_mkLambda_or_LetIn_or_clean (mkApp (mkConst constant, args)) ctx))
+      in
+      true, { obl with obl_body = body }
 
 let init_prog_info ?(opaque = false) sign n udecl b t ctx deps fixkind
 		   notations obls impls kind reduce hook =
@@ -855,7 +856,10 @@ 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 = UState.context ctx 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 (_, obl) = declare_obligation prg obl body ty uctx in
       let obls = Array.copy obls in
       let _ = obls.(num) <- obl in
@@ -967,13 +971,16 @@ and solve_obligation_by_tac prg obls i tac =
 	    let evd = Evd.from_ctx prg.prg_ctx in
 	    let evd = Evd.update_sigma_env evd (Global.env ()) in
 	    let t, ty, ctx =
-	      solve_by_tac obl.obl_name (evar_of_obligation obl) tac
-	        (pi2 prg.prg_kind) (Evd.evar_universe_context evd)
-	    in
-            let uctx = UState.context ctx in
-	    let prg = {prg with prg_ctx = ctx} in
-	    let def, obl' = declare_obligation prg obl t ty uctx in
-	      obls.(i) <- obl';
+              solve_by_tac obl.obl_name (evar_of_obligation obl) tac
+                (pi2 prg.prg_kind) (Evd.evar_universe_context evd)
+            in
+            let uctx = if pi2 prg.prg_kind
+              then Polymorphic_const_entry (UState.context ctx)
+              else Monomorphic_const_entry (UState.context_set ctx)
+            in
+            let prg = {prg with prg_ctx = ctx} in
+            let def, obl' = declare_obligation prg obl t ty uctx in
+              obls.(i) <- obl';
 	      if def && not (pi2 prg.prg_kind) then (
 	        (* Declare the term constraints with the first obligation only *)
 	        let evd = Evd.from_env (Global.env ()) in
@@ -1121,9 +1128,9 @@ let admit_prog prg =
         match x.obl_body with
         | None ->
             let x = subst_deps_obl obls x in
-            let ctx = UState.context prg.prg_ctx in
+            let ctx = Monomorphic_const_entry (UState.context_set prg.prg_ctx) in
             let kn = Declare.declare_constant x.obl_name ~local:true
-              (ParameterEntry (None,false,(x.obl_type,ctx),None), IsAssumption Conjectural)
+              (ParameterEntry (None,(x.obl_type,ctx),None), IsAssumption Conjectural)
             in
               assumption_message x.obl_name;
               obls.(i) <- { x with obl_body = Some (DefinedObl (kn, Univ.Instance.empty)) }
diff --git a/vernac/record.ml b/vernac/record.ml
index 0819dadb4..faf277d86 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -270,7 +270,10 @@ let declare_projections indsp ctx ?(kind=StructureComponent) binder_name coers u
   let env = Global.env() in
   let (mib,mip) = Global.lookup_inductive indsp in
   let poly = Declareops.inductive_is_polymorphic mib in
-  let u = Univ.UContext.instance ctx in
+  let u = match ctx with
+    | Polymorphic_const_entry ctx -> Univ.UContext.instance ctx
+    | Monomorphic_const_entry ctx -> Univ.Instance.empty
+  in
   let paramdecls = Inductive.inductive_paramdecls (mib, u) in
   let indu = indsp, u in
   let r = mkIndU (indsp,u) in
@@ -327,16 +330,12 @@ let declare_projections indsp ctx ?(kind=StructureComponent) binder_name coers u
 		let projtyp =
                   it_mkProd_or_LetIn (mkProd (x,rp,ccl)) paramdecls in
 	        try
-                  let univs =
-                    if poly then Polymorphic_const_entry ctx
-                    else Monomorphic_const_entry ctx
-                  in
 		  let entry = {
 		    const_entry_body =
 		      Future.from_val (Safe_typing.mk_pure_proof proj);
 		    const_entry_secctx = None;
 		    const_entry_type = Some projtyp;
-		    const_entry_universes = univs;
+                    const_entry_universes = ctx;
 		    const_entry_opaque = false;
 		    const_entry_inline_code = false;
 		    const_entry_feedback = None } in
@@ -391,11 +390,14 @@ let declare_structure finite ubinders univs id idbuild paramimpls params arity t
   let args = Context.Rel.to_extended_list mkRel nfields params in
   let ind = applist (mkRel (1+nparams+nfields), args) in
   let type_constructor = it_mkProd_or_LetIn ind fields in
-  let poly, ctx =
+  let template, ctx =
     match univs with
-    | Monomorphic_ind_entry ctx -> false, Univ.UContext.empty
-    | Polymorphic_ind_entry ctx -> true, ctx
-    | Cumulative_ind_entry cumi -> true, (Univ.CumulativityInfo.univ_context cumi)
+    | Monomorphic_ind_entry ctx ->
+      template, Monomorphic_const_entry Univ.ContextSet.empty
+    | Polymorphic_ind_entry ctx ->
+      false, Polymorphic_const_entry ctx
+    | Cumulative_ind_entry cumi ->
+      false, Polymorphic_const_entry (Univ.CumulativityInfo.univ_context cumi)
   in
   let binder_name = 
     match name with
@@ -405,7 +407,7 @@ let declare_structure finite ubinders univs id idbuild paramimpls params arity t
   let mie_ind =
     { mind_entry_typename = id;
       mind_entry_arity = arity;
-      mind_entry_template = not poly && template;
+      mind_entry_template = template;
       mind_entry_consnames = [idbuild];
       mind_entry_lc = [type_constructor] }
   in
@@ -419,14 +421,13 @@ let declare_structure finite ubinders univs id idbuild paramimpls params arity t
     }
   in
   let mie =
-    if poly then
-      begin
+    match ctx with
+    | Polymorphic_const_entry ctx ->
         let env = Global.env () in
         let env' = Environ.push_context ctx env in
         let evd = Evd.from_env env' in
         Inductiveops.infer_inductive_subtyping env' evd mie
-      end
-    else
+    | Monomorphic_const_entry _ ->
        mie
   in
   let kn = Command.declare_mutual_inductive_with_eliminations mie ubinders [(paramimpls,[])] in
@@ -434,6 +435,7 @@ let declare_structure finite ubinders univs id idbuild paramimpls params arity t
   let cstr = (rsp,1) in
   let kinds,sp_projs = declare_projections rsp ctx ~kind binder_name coers ubinders fieldimpls fields in
   let build = ConstructRef cstr in
+  let poly = match ctx with | Polymorphic_const_entry _ -> true | Monomorphic_const_entry _ -> false in
   let () = if is_coe then Class.try_add_new_coercion build ~local:false poly in
   Recordops.declare_structure(rsp,cstr,List.rev kinds,List.rev sp_projs);
   rsp
@@ -499,7 +501,7 @@ let declare_class finite def cum poly ubinders ctx id idbuild paramimpls params
            else
              Polymorphic_ind_entry ctx
          else
-           Monomorphic_ind_entry ctx
+           Monomorphic_ind_entry (Univ.ContextSet.of_context ctx)
        in
        let ind = declare_structure BiFinite ubinders univs (snd id) idbuild paramimpls
 	  params arity template fieldimpls fields
@@ -626,7 +628,7 @@ let definition_structure (kind,cum,poly,finite,(is_coe,((loc,idstruc),pl)),ps,cf
           else
             Polymorphic_ind_entry ctx
         else
-          Monomorphic_ind_entry ctx
+          Monomorphic_ind_entry (Univ.ContextSet.of_context ctx)
       in
       let ind = declare_structure finite pl univs idstruc
 	  idbuild implpars params arity template implfs 
-- 
cgit v1.2.3


From 280c922fc55b57c430cad721c83650a796a375fd Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
Date: Wed, 20 Sep 2017 19:45:43 +0200
Subject: Allow local universe renaming in Print.

---
 doc/refman/RefMan-oth.tex         |  7 +++
 engine/universes.ml               | 15 +++++++
 engine/universes.mli              | 11 +++++
 intf/vernacexpr.ml                |  6 ++-
 parsing/g_vernac.ml4              | 11 +++--
 printing/ppvernac.ml              | 13 ++++--
 printing/prettyp.ml               | 93 +++++++++++++++++++++++----------------
 printing/prettyp.mli              | 10 +++--
 printing/printmod.ml              | 24 ++++++----
 printing/printmod.mli             |  4 +-
 test-suite/output/UnivBinders.out | 31 +++++++++++++
 test-suite/output/UnivBinders.v   | 19 ++++++++
 vernac/vernacentries.ml           | 11 ++---
 13 files changed, 189 insertions(+), 66 deletions(-)

(limited to 'printing')

diff --git a/doc/refman/RefMan-oth.tex b/doc/refman/RefMan-oth.tex
index 60cd8b73a..3ebeba178 100644
--- a/doc/refman/RefMan-oth.tex
+++ b/doc/refman/RefMan-oth.tex
@@ -10,6 +10,8 @@ defined object referred by {\qualid}.
 
 \begin{ErrMsgs}
 \item {\qualid} \errindex{not a defined object}
+\item \errindex{Universe instance should have length} $n$.
+\item \errindex{This object does not support universe names.}
 \end{ErrMsgs}
 
 \begin{Variants}
@@ -27,6 +29,11 @@ constructor, abbreviation, \ldots), long name, type, implicit
 arguments and argument scopes. It does not print the body of
 definitions or proofs.
 
+\item {\tt Print {\qualid}@\{names\}.}\\
+This locally renames the polymorphic universes of {\qualid}.
+An underscore means the raw universe is printed.
+This form can be used with {\tt Print Term} and {\tt About}.
+
 %\item {\tt Print Proof {\qualid}.}\comindex{Print Proof}\\
 %In case \qualid\ denotes an opaque theorem defined in a section,
 %it is stored on a special unprintable form and displayed as 
diff --git a/engine/universes.ml b/engine/universes.ml
index 459c53002..194de2cee 100644
--- a/engine/universes.ml
+++ b/engine/universes.ml
@@ -35,6 +35,21 @@ let universe_binders_of_global ref : universe_binders =
 let register_universe_binders ref l =
   universe_binders_table := Refmap.add ref l !universe_binders_table
 
+type univ_name_list = Name.t Loc.located list
+
+let universe_binders_with_opt_names ref levels = function
+  | None -> universe_binders_of_global ref
+  | Some udecl ->
+    if Int.equal(List.length levels) (List.length udecl)
+    then
+      List.fold_left2 (fun acc (_,na) lvl -> match na with
+          | Anonymous -> acc
+          | Name na -> Names.Id.Map.add na lvl acc)
+        empty_binders udecl levels
+    else
+      CErrors.user_err ~hdr:"universe_binders_with_opt_names"
+        Pp.(str "Universe instance should have length " ++ int (List.length levels))
+
 (* To disallow minimization to Set *)
 
 let set_minimization = ref true
diff --git a/engine/universes.mli b/engine/universes.mli
index 621ca5e84..1401c4ee8 100644
--- a/engine/universes.mli
+++ b/engine/universes.mli
@@ -28,6 +28,17 @@ val empty_binders : universe_binders
 val register_universe_binders : Globnames.global_reference -> universe_binders -> unit
 val universe_binders_of_global : Globnames.global_reference -> universe_binders
 
+type univ_name_list = Name.t Loc.located list
+
+(** [universe_binders_with_opt_names ref u l]
+
+    If [l] is [Some univs] return the universe binders naming the levels of [u] by [univs] (skipping Anonymous).
+    May error if the lengths mismatch.
+
+    Otherwise return [universe_binders_of_global ref]. *)
+val universe_binders_with_opt_names : Globnames.global_reference ->
+  Univ.Level.t list -> univ_name_list option -> universe_binders
+
 (** The global universe counter *)
 val set_remote_new_univ_level : Level.t RemoteCounter.installer
 
diff --git a/intf/vernacexpr.ml b/intf/vernacexpr.ml
index 9aef4b131..96bcba5e8 100644
--- a/intf/vernacexpr.ml
+++ b/intf/vernacexpr.ml
@@ -40,6 +40,8 @@ type goal_reference =
   | NthGoal of int
   | GoalId of Id.t
 
+type univ_name_list = Name.t Loc.located list
+
 type printable =
   | PrintTables
   | PrintFullContext
@@ -54,7 +56,7 @@ type printable =
   | PrintMLLoadPath
   | PrintMLModules
   | PrintDebugGC
-  | PrintName of reference or_by_notation
+  | PrintName of reference or_by_notation * univ_name_list option
   | PrintGraph
   | PrintClasses
   | PrintTypeClasses
@@ -70,7 +72,7 @@ type printable =
   | PrintScopes
   | PrintScope of string
   | PrintVisibility of string option
-  | PrintAbout of reference or_by_notation * goal_selector option
+  | PrintAbout of reference or_by_notation * univ_name_list option * goal_selector option
   | PrintImplicit of reference or_by_notation
   | PrintAssumptions of bool * bool * reference or_by_notation
   | PrintStrategy of reference or_by_notation option
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index a01ea26af..0e585cff7 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -875,7 +875,7 @@ GEXTEND Gram
 
       (* Printing (careful factorization of entries) *)
       | IDENT "Print"; p = printable -> VernacPrint p
-      | IDENT "Print"; qid = smart_global -> VernacPrint (PrintName qid)
+      | IDENT "Print"; qid = smart_global; l = OPT univ_name_list -> VernacPrint (PrintName (qid,l))
       | IDENT "Print"; IDENT "Module"; "Type"; qid = global ->
 	  VernacPrint (PrintModuleType qid)
       | IDENT "Print"; IDENT "Module"; qid = global ->
@@ -940,8 +940,8 @@ GEXTEND Gram
       | IDENT "Check"; c = lconstr; "." ->
 	 fun g -> VernacCheckMayEval (None, g, c)
       (* Searching the environment *)
-      | IDENT "About"; qid = smart_global; "." ->
-	 fun g -> VernacPrint (PrintAbout (qid,g))
+      | IDENT "About"; qid = smart_global; l = OPT univ_name_list; "." ->
+         fun g -> VernacPrint (PrintAbout (qid,l,g))
       | IDENT "SearchHead"; c = constr_pattern; l = in_or_out_modules; "." ->
 	  fun g -> VernacSearch (SearchHead c,g, l)
       | IDENT "SearchPattern"; c = constr_pattern; l = in_or_out_modules; "." ->
@@ -960,7 +960,7 @@ GEXTEND Gram
       ] ]
   ;
   printable:
-    [ [ IDENT "Term"; qid = smart_global -> PrintName qid
+    [ [ IDENT "Term"; qid = smart_global; l = OPT univ_name_list -> PrintName (qid,l)
       | IDENT "All" -> PrintFullContext
       | IDENT "Section"; s = global -> PrintSectionContext s
       | IDENT "Grammar"; ent = IDENT ->
@@ -1060,6 +1060,9 @@ GEXTEND Gram
       | -> ([],SearchOutside [])
       ] ]
   ;
+  univ_name_list:
+    [ [  "@{" ; l = LIST0 name; "}" -> l ] ]
+  ;
 END;
 
 GEXTEND Gram
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index e897b1938..1a74538aa 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -41,6 +41,11 @@ open Decl_kinds
     pr_glob_level l ++ spc () ++ Univ.pr_constraint_type d ++ spc () ++
       pr_glob_level r
 
+  let pr_univ_name_list = function
+    | None -> mt ()
+    | Some l ->
+      str "@{" ++ prlist_with_sep spc pr_lname l ++ str"}"
+
   let pr_univdecl_instance l extensible =
     prlist_with_sep spc pr_lident l ++
     (if extensible then str"+" else mt ())
@@ -488,8 +493,8 @@ open Decl_kinds
         else "Print Universes"
       in
       keyword cmd ++ pr_opt str fopt
-    | PrintName qid ->
-      keyword "Print" ++ spc()  ++ pr_smart_global qid
+    | PrintName (qid,udecl) ->
+      keyword "Print" ++ spc()  ++ pr_smart_global qid ++ pr_univ_name_list udecl
     | PrintModuleType qid ->
       keyword "Print Module Type" ++ spc() ++ pr_reference qid
     | PrintModule qid ->
@@ -502,9 +507,9 @@ open Decl_kinds
       keyword "Print Scope" ++ spc() ++ str s
     | PrintVisibility s ->
       keyword "Print Visibility" ++ pr_opt str s
-    | PrintAbout (qid,gopt) ->
+    | PrintAbout (qid,l,gopt) ->
        pr_opt (fun g -> Proof_bullet.pr_goal_selector g ++ str ":"++ spc()) gopt
-       ++ keyword "About" ++ spc()  ++ pr_smart_global qid
+       ++ keyword "About" ++ spc()  ++ pr_smart_global qid ++ pr_univ_name_list l
     | PrintImplicit qid ->
       keyword "Print Implicit" ++ spc()  ++ pr_smart_global qid
     (* spiwack: command printing all the axioms and section variables used in a
diff --git a/printing/prettyp.ml b/printing/prettyp.ml
index b4ac94103..602b7a496 100644
--- a/printing/prettyp.ml
+++ b/printing/prettyp.ml
@@ -32,8 +32,8 @@ open Context.Rel.Declaration
 module NamedDecl = Context.Named.Declaration
 
 type object_pr = {
-  print_inductive           : MutInd.t -> Pp.t;
-  print_constant_with_infos : Constant.t -> Pp.t;
+  print_inductive           : MutInd.t -> Universes.univ_name_list option -> Pp.t;
+  print_constant_with_infos : Constant.t -> Universes.univ_name_list option -> Pp.t;
   print_section_variable    : env -> Evd.evar_map -> variable -> Pp.t;
   print_syntactic_def       : env -> KerName.t -> Pp.t;
   print_module              : bool -> ModPath.t -> Pp.t;
@@ -68,7 +68,7 @@ let int_or_no n = if Int.equal n 0 then str "no" else int n
 
 let print_basename sp = pr_global (ConstRef sp)
 
-let print_ref reduce ref =
+let print_ref reduce ref udecl =
   let typ, ctx = Global.type_of_global_in_context (Global.env ()) ref in
   let typ = Vars.subst_instance_constr (Univ.AUContext.instance ctx) typ in
   let typ = EConstr.of_constr typ in
@@ -81,7 +81,8 @@ let print_ref reduce ref =
   let inst = Univ.AUContext.instance univs in
   let univs = Univ.UContext.make (inst, Univ.AUContext.instantiate inst univs) in
   let env = Global.env () in
-  let bl = Universes.universe_binders_of_global ref in
+  let bl = Universes.universe_binders_with_opt_names ref
+      (Array.to_list (Univ.Instance.to_array inst)) udecl in
   let sigma = Evd.from_ctx (Evd.evar_universe_context_of_binders bl) in
   let inst =
     if Global.is_polymorphic ref then Printer.pr_universe_instance sigma univs
@@ -150,7 +151,7 @@ let print_impargs ref =
   let has_impl = not (List.is_empty impl) in
   (* Need to reduce since implicits are computed with products flattened *)
   pr_infos_list
-    ([ print_ref (need_expansion (select_impargs_size 0 impl) ref) ref;
+    ([ print_ref (need_expansion (select_impargs_size 0 impl) ref) ref None;
        blankline ] @
     (if has_impl then print_impargs_list (mt()) impl
      else [str "No implicit arguments"]))
@@ -256,7 +257,7 @@ let print_name_infos ref =
     if need_expansion (select_impargs_size 0 impls) ref then
       (* Need to reduce since implicits are computed with products flattened *)
       [str "Expanded type for implicit arguments";
-       print_ref true ref; blankline]
+       print_ref true ref None; blankline]
     else
       [] in
   print_polymorphism ref @
@@ -512,11 +513,11 @@ let assumptions_for_print lna =
 (*********************)
 (* *)
 
-let gallina_print_inductive sp =
+let gallina_print_inductive sp udecl =
   let env = Global.env() in
   let mib = Environ.lookup_mind sp env in
   let mipv = mib.mind_packets in
-  pr_mutual_inductive_body env sp mib ++
+  pr_mutual_inductive_body env sp mib udecl ++
   with_line_skip
     (print_primitive_record mib.mind_finite mipv mib.mind_record @
      print_inductive_renames sp mipv @
@@ -545,7 +546,7 @@ let print_instance sigma cb =
     pr_universe_instance sigma univs
   else mt()
 				
-let print_constant with_values sep sp =
+let print_constant with_values sep sp udecl =
   let cb = Global.lookup_constant sp in
   let val_0 = Global.body_of_constant_body cb in
   let typ =
@@ -555,31 +556,34 @@ let print_constant with_values sep sp =
       let inst = Univ.AUContext.instance univs in
       Vars.subst_instance_constr inst cb.const_type
   in
-  let univs =
+  let univs, ulist =
     let open Entries in
+    let open Univ in
     let otab = Global.opaque_tables () in
     match cb.const_body with
     | Undef _ | Def _ ->
       begin
         match cb.const_universes with
-        | Monomorphic_const ctx -> Monomorphic_const_entry ctx
+        | Monomorphic_const ctx -> Monomorphic_const_entry ctx, []
         | Polymorphic_const ctx ->
-          let inst = Univ.AUContext.instance ctx in
-          Polymorphic_const_entry (Univ.UContext.make (inst, Univ.AUContext.instantiate inst ctx))
+          let inst = AUContext.instance ctx in
+          Polymorphic_const_entry (UContext.make (inst, AUContext.instantiate inst ctx)),
+          Array.to_list (Instance.to_array inst)
       end
     | OpaqueDef o ->
       let body_uctxs = Opaqueproof.force_constraints otab o in
       match cb.const_universes with
       | Monomorphic_const ctx ->
-        Monomorphic_const_entry (Univ.ContextSet.union body_uctxs ctx)
+        Monomorphic_const_entry (ContextSet.union body_uctxs ctx), []
       | Polymorphic_const ctx ->
-        assert(Univ.ContextSet.is_empty body_uctxs);
-        let inst = Univ.AUContext.instance ctx in
-        Polymorphic_const_entry (Univ.UContext.make (inst, Univ.AUContext.instantiate inst ctx))
+        assert(ContextSet.is_empty body_uctxs);
+        let inst = AUContext.instance ctx in
+        Polymorphic_const_entry (UContext.make (inst, AUContext.instantiate inst ctx)),
+        Array.to_list (Instance.to_array inst)
   in
   let ctx =
     Evd.evar_universe_context_of_binders
-      (Universes.universe_binders_of_global (ConstRef sp))
+      (Universes.universe_binders_with_opt_names (ConstRef sp) ulist udecl)
   in
   let env = Global.env () and sigma = Evd.from_ctx ctx in
   let pr_ltype = pr_ltype_env env sigma in
@@ -596,8 +600,8 @@ let print_constant with_values sep sp =
 	(if with_values then print_typed_body env sigma (Some c,typ) else pr_ltype typ)++
         Printer.pr_constant_universes sigma univs)
 
-let gallina_print_constant_with_infos sp =
-  print_constant true " = " sp ++
+let gallina_print_constant_with_infos sp udecl =
+  print_constant true " = " sp udecl ++
   with_line_skip (print_name_infos (ConstRef sp))
 
 let gallina_print_syntactic_def env kn =
@@ -622,9 +626,9 @@ let gallina_print_leaf_entry env sigma with_values ((sp,kn as oname),lobj) =
              constraints *)
           (try Some(print_named_decl env sigma (basename sp)) with Not_found -> None)
       | (_,"CONSTANT") ->
-	  Some (print_constant with_values sep (Constant.make1 kn))
+          Some (print_constant with_values sep (Constant.make1 kn) None)
       | (_,"INDUCTIVE") ->
-	  Some (gallina_print_inductive (MutInd.make1 kn))
+          Some (gallina_print_inductive (MutInd.make1 kn) None)
       | (_,"MODULE") ->
 	  let (mp,_,l) = KerName.repr kn in
 	    Some (print_module with_values (MPdot (mp,l)))
@@ -745,7 +749,7 @@ let print_full_pure_context env sigma =
       | "INDUCTIVE" ->
 	  let mind = Global.mind_of_delta_kn kn in
 	  let mib = Global.lookup_mind mind in
-	  pr_mutual_inductive_body (Global.env()) mind mib ++
+          pr_mutual_inductive_body (Global.env()) mind mib None ++
 	    str "." ++ fnl () ++ fnl ()
       | "MODULE" ->
 	  (* TODO: make it reparsable *)
@@ -792,10 +796,19 @@ let print_sec_context env sigma sec =
 let print_sec_context_typ env sigma sec =
   print_context env sigma false None (read_sec_context sec)
 
-let print_any_name env sigma = function
-  | Term (ConstRef sp) -> print_constant_with_infos sp
-  | Term (IndRef (sp,_)) -> print_inductive sp
-  | Term (ConstructRef ((sp,_),_)) -> print_inductive sp
+let maybe_error_reject_univ_decl na udecl =
+  match na, udecl with
+  | _, None | Term (ConstRef _ | IndRef _ | ConstructRef _), Some _ -> ()
+  | (Term (VarRef _) | Syntactic _ | Dir _ | ModuleType _ | Other _ | Undefined _), Some udecl ->
+    (* TODO Print na somehow *)
+    user_err ~hdr:"reject_univ_decl" (str "This object does not support universe names.")
+
+let print_any_name env sigma na udecl =
+  maybe_error_reject_univ_decl na udecl;
+  match na with
+  | Term (ConstRef sp) -> print_constant_with_infos sp udecl
+  | Term (IndRef (sp,_)) -> print_inductive sp udecl
+  | Term (ConstructRef ((sp,_),_)) -> print_inductive sp udecl
   | Term (VarRef sp) -> print_section_variable env sigma sp
   | Syntactic kn -> print_syntactic_def env kn
   | Dir (DirModule(dirpath,(mp,_))) -> print_module (printable_body dirpath) mp
@@ -812,24 +825,26 @@ let print_any_name env sigma = function
     user_err
       ~hdr:"print_name" (pr_qualid qid ++ spc () ++ str "not a defined object.")
 
-let print_name env sigma = function
+let print_name env sigma na udecl =
+  match na with
   | ByNotation (loc,(ntn,sc)) ->
       print_any_name env sigma
         (Term (Notation.interp_notation_as_global_reference ?loc (fun _ -> true)
                ntn sc))
+        udecl
   | AN ref ->
-      print_any_name env sigma (locate_any_name ref)
+      print_any_name env sigma (locate_any_name ref) udecl
 
 let print_opaque_name env sigma qid =
   match Nametab.global qid with
     | ConstRef cst ->
 	let cb = Global.lookup_constant cst in
         if Declareops.constant_has_body cb then
-	  print_constant_with_infos cst
+          print_constant_with_infos cst None
         else
 	  user_err Pp.(str "Not a defined constant.")
     | IndRef (sp,_) ->
-        print_inductive sp
+        print_inductive sp None
     | ConstructRef cstr as gr ->
 	let ty, ctx = Global.type_of_global_in_context env gr in
 	let inst = Univ.AUContext.instance ctx in
@@ -840,13 +855,14 @@ let print_opaque_name env sigma qid =
     | VarRef id ->
         env |> lookup_named id |> print_named_decl env sigma
 
-let print_about_any ?loc env sigma k =
+let print_about_any ?loc env sigma k udecl =
+  maybe_error_reject_univ_decl k udecl;
   match k with
   | Term ref ->
     let rb = Reductionops.ReductionBehaviour.print ref in
     Dumpglob.add_glob ?loc ref;
       pr_infos_list
-       (print_ref false ref :: blankline ::
+       (print_ref false ref udecl :: blankline ::
 	print_name_infos ref @
 	(if Pp.ismt rb then [] else [rb]) @
 	print_opacity ref @
@@ -862,13 +878,14 @@ let print_about_any ?loc env sigma k =
       hov 0 (pr_located_qualid k)
   | Other (obj, info) -> hov 0 (info.about obj)
 
-let print_about env sigma = function
+let print_about env sigma na udecl =
+  match na with
   | ByNotation (loc,(ntn,sc)) ->
       print_about_any ?loc env sigma
         (Term (Notation.interp_notation_as_global_reference ?loc (fun _ -> true)
-               ntn sc))
+               ntn sc)) udecl
   | AN ref ->
-      print_about_any ?loc:(loc_of_reference ref) env sigma (locate_any_name ref)
+      print_about_any ?loc:(loc_of_reference ref) env sigma (locate_any_name ref) udecl
 
 (* for debug *)
 let inspect env sigma depth =
@@ -940,7 +957,7 @@ let print_canonical_projections env sigma =
 open Typeclasses
 
 let pr_typeclass env t =
-  print_ref false t.cl_impl
+  print_ref false t.cl_impl None
 
 let print_typeclasses () =
   let env = Global.env () in
@@ -949,7 +966,7 @@ let print_typeclasses () =
 let pr_instance env i =
   (*   gallina_print_constant_with_infos i.is_impl *)
   (* lighter *)
-  print_ref false (instance_impl i) ++
+  print_ref false (instance_impl i) None ++
   begin match hint_priority i with
   | None -> mt ()
   | Some i -> spc () ++ str "|" ++ spc () ++ int i
diff --git a/printing/prettyp.mli b/printing/prettyp.mli
index 89099a043..8f3a6ddc4 100644
--- a/printing/prettyp.mli
+++ b/printing/prettyp.mli
@@ -31,9 +31,11 @@ val print_eval :
   reduction_function -> env -> Evd.evar_map ->
     Constrexpr.constr_expr -> EConstr.unsafe_judgment -> Pp.t
 
-val print_name : env -> Evd.evar_map -> reference or_by_notation -> Pp.t
+val print_name : env -> Evd.evar_map -> reference or_by_notation ->
+  Vernacexpr.univ_name_list option -> Pp.t
 val print_opaque_name : env -> Evd.evar_map -> reference -> Pp.t
-val print_about : env -> Evd.evar_map -> reference or_by_notation -> Pp.t
+val print_about : env -> Evd.evar_map -> reference or_by_notation ->
+  Vernacexpr.univ_name_list option -> Pp.t
 val print_impargs : reference or_by_notation -> Pp.t
 
 (** Pretty-printing functions for classes and coercions *)
@@ -80,8 +82,8 @@ val print_located_module : reference -> Pp.t
 val print_located_other : string -> reference -> Pp.t
 
 type object_pr = {
-  print_inductive           : MutInd.t -> Pp.t;
-  print_constant_with_infos : Constant.t -> Pp.t;
+  print_inductive           : MutInd.t -> Universes.univ_name_list option -> Pp.t;
+  print_constant_with_infos : Constant.t -> Universes.univ_name_list option -> Pp.t;
   print_section_variable    : env -> Evd.evar_map -> variable -> Pp.t;
   print_syntactic_def       : env -> KerName.t -> Pp.t;
   print_module              : bool -> ModPath.t -> Pp.t;
diff --git a/printing/printmod.ml b/printing/printmod.ml
index 13a03e9b4..c34543bbd 100644
--- a/printing/printmod.ml
+++ b/printing/printmod.ml
@@ -121,7 +121,7 @@ let instantiate_cumulativity_info cumi =
   in
   CumulativityInfo.make (expose univs, expose subtyp)
 
-let print_mutual_inductive env mind mib =
+let print_mutual_inductive env mind mib udecl =
   let inds = List.init (Array.length mib.mind_packets) (fun x -> (mind, x))
   in
   let keyword =
@@ -131,7 +131,14 @@ let print_mutual_inductive env mind mib =
     | BiFinite -> "Variant"
     | CoFinite -> "CoInductive"
   in
-  let bl = Universes.universe_binders_of_global (IndRef (mind, 0)) in
+  let univs =
+    let open Univ in
+    if Declareops.inductive_is_polymorphic mib then
+      Array.to_list (Instance.to_array
+                       (AUContext.instance (Declareops.inductive_polymorphic_context mib)))
+    else []
+  in
+  let bl = Universes.universe_binders_with_opt_names (IndRef (mind, 0)) univs udecl in
   let sigma = Evd.from_ctx (Evd.evar_universe_context_of_binders bl) in
   hov 0 (Printer.pr_polymorphic (Declareops.inductive_is_polymorphic mib) ++
          Printer.pr_cumulative
@@ -159,7 +166,7 @@ let get_fields =
   in
   prodec_rec [] []
 
-let print_record env mind mib =
+let print_record env mind mib udecl =
   let u = 
     if Declareops.inductive_is_polymorphic mib then 
       Univ.AUContext.instance (Declareops.inductive_polymorphic_context mib)
@@ -173,7 +180,8 @@ let print_record env mind mib =
   let cstrtype = hnf_prod_applist env cstrtypes.(0) args in
   let fields = get_fields cstrtype in
   let envpar = push_rel_context params env in
-  let bl = Universes.universe_binders_of_global (IndRef (mind,0)) in
+  let bl = Universes.universe_binders_with_opt_names (IndRef (mind,0))
+      (Array.to_list (Univ.Instance.to_array u)) udecl in
   let sigma = Evd.from_ctx (Evd.evar_universe_context_of_binders bl) in
   let keyword =
     let open Decl_kinds in
@@ -205,11 +213,11 @@ let print_record env mind mib =
         sigma (instantiate_cumulativity_info cumi)
   )
 
-let pr_mutual_inductive_body env mind mib =
+let pr_mutual_inductive_body env mind mib udecl =
   if mib.mind_record <> None && not !Flags.raw_print then
-    print_record env mind mib
+    print_record env mind mib udecl
   else
-    print_mutual_inductive env mind mib
+    print_mutual_inductive env mind mib udecl
 
 (** Modpaths *)
 
@@ -335,7 +343,7 @@ let print_body is_impl env mp (l,body) =
     | SFBmind mib ->
       try
 	let env = Option.get env in
-	pr_mutual_inductive_body env (MutInd.make2 mp l) mib
+        pr_mutual_inductive_body env (MutInd.make2 mp l) mib None
       with e when CErrors.noncritical e ->
         let keyword =
           let open Decl_kinds in
diff --git a/printing/printmod.mli b/printing/printmod.mli
index b0bbb21e0..97ed063fe 100644
--- a/printing/printmod.mli
+++ b/printing/printmod.mli
@@ -11,6 +11,8 @@ open Names
 (** false iff the module is an element of an open module type *)
 val printable_body : DirPath.t -> bool
 
-val pr_mutual_inductive_body : Environ.env -> MutInd.t -> Declarations.mutual_inductive_body -> Pp.t
+val pr_mutual_inductive_body : Environ.env ->
+  MutInd.t -> Declarations.mutual_inductive_body ->
+  Vernacexpr.univ_name_list option -> Pp.t
 val print_module : bool -> ModPath.t -> Pp.t
 val print_modtype : ModPath.t -> Pp.t
diff --git a/test-suite/output/UnivBinders.out b/test-suite/output/UnivBinders.out
index 42fb52a3b..6fb8cba18 100644
--- a/test-suite/output/UnivBinders.out
+++ b/test-suite/output/UnivBinders.out
@@ -53,3 +53,34 @@ Monomorphic mono = Type@{u}
 (* {u} |=  *)
 
 mono is not universe polymorphic
+foo@{E M N} = 
+Type@{M} -> Type@{N} -> Type@{E}
+     : Type@{max(E+1, M+1, N+1)}
+(* E M N |=  *)
+
+foo is universe polymorphic
+foo@{Top.16 Top.17 Top.18} = 
+Type@{Top.17} -> Type@{Top.18} -> Type@{Top.16}
+     : Type@{max(Top.16+1, Top.17+1, Top.18+1)}
+(* Top.16 Top.17 Top.18 |=  *)
+
+foo is universe polymorphic
+NonCumulative Inductive Empty@{E} : Type@{E} :=  
+NonCumulative Record PWrap (A : Type@{E}) : Type@{E} := pwrap { punwrap : A }
+
+PWrap has primitive projections with eta conversion.
+For PWrap: Argument scope is [type_scope]
+For pwrap: Argument scopes are [type_scope _]
+punwrap@{K} : forall A : Type@{K}, PWrap@{K} A -> A
+(* K |=  *)
+
+punwrap is universe polymorphic
+Argument scopes are [type_scope _]
+punwrap is transparent
+Expands to: Constant Top.punwrap
+The command has indeed failed with message:
+Universe instance should have length 3
+The command has indeed failed with message:
+Universe instance should have length 0
+The command has indeed failed with message:
+This object does not support universe names.
diff --git a/test-suite/output/UnivBinders.v b/test-suite/output/UnivBinders.v
index 2c378e795..46904b384 100644
--- a/test-suite/output/UnivBinders.v
+++ b/test-suite/output/UnivBinders.v
@@ -33,3 +33,22 @@ Print foo.
 (* Binders even work with monomorphic definitions! *)
 Monomorphic Definition mono@{u} := Type@{u}.
 Print mono.
+
+(* Using local binders for printing. *)
+Print foo@{E M N}.
+(* Underscores discard the name if there's one. *)
+Print foo@{_ _ _}.
+
+(* Also works for inductives and records. *)
+Print Empty@{E}.
+Print PWrap@{E}.
+
+(* Also works for About. *)
+About punwrap@{K}.
+
+(* Instance length check. *)
+Fail Print foo@{E}.
+Fail Print mono@{E}.
+
+(* Not everything can be printed with custom universe names. *)
+Fail Print Coq.Init.Logic@{E}.
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index e2f28a371..22e3e9c99 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -1609,9 +1609,10 @@ exception NoHyp
 (* Printing "About" information of a hypothesis of the current goal.
    We only print the type and a small statement to this comes from the
    goal. Precondition: there must be at least one current goal. *)
-let print_about_hyp_globs ?loc ref_or_by_not glopt =
+let print_about_hyp_globs ?loc ref_or_by_not udecl glopt =
   let open Context.Named.Declaration in
   try
+    (* FIXME error on non None udecl if we find the hyp. *)
     let glnumopt = query_command_selector ?loc glopt in
     let gl,id =
       match glnumopt,ref_or_by_not with
@@ -1634,7 +1635,7 @@ let print_about_hyp_globs ?loc ref_or_by_not glopt =
   with (* fallback to globals *)
     | NoHyp | Not_found ->
     let sigma, env = Pfedit.get_current_context () in
-    print_about env sigma ref_or_by_not
+    print_about env sigma ref_or_by_not udecl
 
 
 let vernac_print ?loc env sigma = let open Feedback in function
@@ -1651,7 +1652,7 @@ let vernac_print ?loc env sigma = let open Feedback in function
   | PrintMLLoadPath -> msg_notice (Mltop.print_ml_path ())
   | PrintMLModules -> msg_notice (Mltop.print_ml_modules ())
   | PrintDebugGC -> msg_notice (Mltop.print_gc ())
-  | PrintName qid -> dump_global qid; msg_notice (print_name env sigma qid)
+  | PrintName (qid,udecl) -> dump_global qid; msg_notice (print_name env sigma qid udecl)
   | PrintGraph -> msg_notice (Prettyp.print_graph())
   | PrintClasses -> msg_notice (Prettyp.print_classes())
   | PrintTypeClasses -> msg_notice (Prettyp.print_typeclasses())
@@ -1681,8 +1682,8 @@ let vernac_print ?loc env sigma = let open Feedback in function
       msg_notice (Notation.pr_scope (Constrextern.without_symbols (pr_lglob_constr_env env)) s)
   | PrintVisibility s ->
       msg_notice (Notation.pr_visibility (Constrextern.without_symbols (pr_lglob_constr_env env)) s)
-  | PrintAbout (ref_or_by_not,glnumopt) ->
-     msg_notice (print_about_hyp_globs ?loc ref_or_by_not glnumopt)
+  | PrintAbout (ref_or_by_not,udecl,glnumopt) ->
+     msg_notice (print_about_hyp_globs ?loc ref_or_by_not udecl glnumopt)
   | PrintImplicit qid ->
     dump_global qid; msg_notice (print_impargs qid)
   | PrintAssumptions (o,t,r) ->
-- 
cgit v1.2.3