Merge PR #8475: Centralize the reliance on abstract universe context internals

13 files changed, 129 insertions, 144 deletions

diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst
index 837d3f10a2..be65ff7570 100644
--- a/doc/sphinx/proof-engine/vernacular-commands.rst
+++ b/doc/sphinx/proof-engine/vernacular-commands.rst
@@ -35,7 +35,7 @@ Displaying
    .. cmdv:: Print {? Term } @qualid\@@name
 
       This locally renames the polymorphic universes of :n:`@qualid`.
-      An underscore means the raw universe is printed.
+      An underscore means the usual name is printed.
 
 
 .. cmd:: About @qualid
@@ -49,7 +49,7 @@ Displaying
    .. cmdv:: About @qualid\@@name
 
       This locally renames the polymorphic universes of :n:`@qualid`.
-      An underscore means the raw universe is printed.
+      An underscore means the usual name is printed.
 
 
 .. cmd:: Print All
diff --git a/engine/univNames.ml b/engine/univNames.ml
index e861913de2..9e4c6e47fc 100644
--- a/engine/univNames.ml
+++ b/engine/univNames.ml
@@ -8,6 +8,7 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
+open Util
 open Names
 open Univ
 open Nametab
@@ -52,10 +53,10 @@ let empty_binders = Id.Map.empty
 
 let universe_binders_table = Summary.ref GlobRef.Map.empty ~name:"universe binders"
 
-let universe_binders_of_global ref : universe_binders =
+let universe_binders_of_global ref : Id.t list =
   try
     let l = GlobRef.Map.find ref !universe_binders_table in l
-  with Not_found -> Names.Id.Map.empty
+  with Not_found -> []
 
 let cache_ubinder (_,(ref,l)) =
   universe_binders_table := GlobRef.Map.add ref l !universe_binders_table
@@ -64,10 +65,28 @@ let subst_ubinder (subst,(ref,l as orig)) =
   let ref' = fst (Globnames.subst_global subst ref) in
   if ref == ref' then orig else ref', l
 
+let name_universe lvl =
+  (** Best-effort naming from the string representation of the level. This is
+      completely hackish and should be solved in upper layers instead. *)
+  Id.of_string_soft (Level.to_string lvl)
+
 let discharge_ubinder (_,(ref,l)) =
+  (** Expand polymorphic binders with the section context *)
+  let info = Lib.section_segment_of_reference ref in
+  let sec_inst = Array.to_list (Instance.to_array (info.Lib.abstr_subst)) in
+  let map lvl = match Level.name lvl with
+    | None -> (* Having Prop/Set/Var as section universes makes no sense *)
+      assert false
+    | Some na ->
+      try
+        let qid = Nametab.shortest_qualid_of_universe na in
+        snd (Libnames.repr_qualid qid)
+      with Not_found -> name_universe lvl
+  in
+  let l = List.map map sec_inst @ l in
   Some (Lib.discharge_global ref, l)
 
-let ubinder_obj : GlobRef.t * universe_binders -> Libobject.obj =
+let ubinder_obj : GlobRef.t * Id.t list -> Libobject.obj =
   let open Libobject in
   declare_object { (default_object "universe binder") with
     cache_function = cache_ubinder;
@@ -78,28 +97,35 @@ let ubinder_obj : GlobRef.t * universe_binders -> Libobject.obj =
     rebuild_function = (fun x -> x); }
 
 let register_universe_binders ref ubinders =
-  (* Add the polymorphic (section) universes *)
-  let ubinders = UnivIdMap.fold (fun lvl poly ubinders ->
-    let qid = Nametab.shortest_qualid_of_universe lvl in
-    let level = Level.make (fst lvl) (snd lvl) in
-    if poly then Id.Map.add (snd (Libnames.repr_qualid qid)) level ubinders
-    else ubinders)
-    !universe_map ubinders
+  (** TODO: change the API to register a [Name.t list] instead. This is the last
+      part of the code that depends on the internal representation of names in
+      abstract contexts, but removing it requires quite a rework of the
+      callers. *)
+  let univs = AUContext.instance (Global.universes_of_global ref) in
+  let revmap = Id.Map.fold (fun id lvl accu -> LMap.add lvl id accu) ubinders LMap.empty in
+  let map lvl =
+    try LMap.find lvl revmap
+    with Not_found -> name_universe lvl
   in
-  if not (Id.Map.is_empty ubinders)
-  then Lib.add_anonymous_leaf (ubinder_obj (ref,ubinders))
+  let ubinders = Array.map_to_list map (Instance.to_array univs) in
+  if not (List.is_empty ubinders) then Lib.add_anonymous_leaf (ubinder_obj (ref, ubinders))
 
 type univ_name_list = Names.lname list
 
-let universe_binders_with_opt_names ref levels = function
-  | None -> universe_binders_of_global ref
+let universe_binders_with_opt_names ref names =
+  let orig = universe_binders_of_global ref in
+  let udecl = match names with
+  | None -> orig
   | Some udecl ->
-    if Int.equal(List.length levels) (List.length udecl)
-    then
-      List.fold_left2 (fun acc { CAst.v = na} lvl -> match na with
-          | Anonymous -> acc
-          | Name na -> Names.Id.Map.add na lvl acc)
-        empty_binders udecl levels
-    else
+    try
+      List.map2 (fun orig {CAst.v = na} ->
+          match na with
+          | Anonymous -> orig
+          | Name id -> id) orig udecl
+    with Invalid_argument _ ->
+      let len = List.length orig in
       CErrors.user_err ~hdr:"universe_binders_with_opt_names"
-        Pp.(str "Universe instance should have length " ++ int (List.length levels))
+        Pp.(str "Universe instance should have length " ++ int len)
+  in
+  let fold i acc na = Names.Id.Map.add na (Level.var i) acc in
+  List.fold_left_i fold 0 empty_binders udecl
diff --git a/engine/univNames.mli b/engine/univNames.mli
index 837beac267..d794d7b744 100644
--- a/engine/univNames.mli
+++ b/engine/univNames.mli
@@ -27,15 +27,14 @@ type universe_binders = Univ.Level.t Names.Id.Map.t
 val empty_binders : universe_binders
 
 val register_universe_binders : Names.GlobRef.t -> universe_binders -> unit
-val universe_binders_of_global : Names.GlobRef.t -> universe_binders
 
 type univ_name_list = Names.lname list
 
-(** [universe_binders_with_opt_names ref u l]
+(** [universe_binders_with_opt_names ref 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.
+    If [l] is [Some univs] return the universe binders naming the bound levels
+    of [ref] by [univs] (skipping Anonymous). May error if the lengths mismatch.
 
-    Otherwise return [universe_binders_of_global ref]. *)
+    Otherwise return the bound universe names registered for [ref]. *)
 val universe_binders_with_opt_names : Names.GlobRef.t ->
-  Univ.Level.t list -> univ_name_list option -> universe_binders
+  univ_name_list option -> universe_binders
diff --git a/engine/universes.ml b/engine/universes.ml
index ee9668433c..c7e5f654a1 100644
--- a/engine/universes.ml
+++ b/engine/universes.ml
@@ -26,7 +26,6 @@ let is_polymorphic = UnivNames.is_polymorphic
 let empty_binders = UnivNames.empty_binders
 
 let register_universe_binders = UnivNames.register_universe_binders
-let universe_binders_of_global = UnivNames.universe_binders_of_global
 
 let universe_binders_with_opt_names = UnivNames.universe_binders_with_opt_names
 
diff --git a/engine/universes.mli b/engine/universes.mli
index ad937471e9..7ca33f47a1 100644
--- a/engine/universes.mli
+++ b/engine/universes.mli
@@ -39,14 +39,12 @@ val empty_binders : universe_binders
 
 val register_universe_binders : Globnames.global_reference -> universe_binders -> unit
 [@@ocaml.deprecated "Use [UnivNames.register_universe_binders]"]
-val universe_binders_of_global : Globnames.global_reference -> universe_binders
-[@@ocaml.deprecated "Use [UnivNames.universe_binders_of_global]"]
 
 type univ_name_list = UnivNames.univ_name_list
 [@@ocaml.deprecated "Use [UnivNames.univ_name_list]"]
 
 val universe_binders_with_opt_names : Globnames.global_reference ->
-  Univ.Level.t list -> univ_name_list option -> universe_binders
+  univ_name_list option -> universe_binders
 [@@ocaml.deprecated "Use [UnivNames.universe_binders_with_opt_names]"]
 
 (** ****** Deprecated: moved to [UnivGen] *)
diff --git a/kernel/univ.ml b/kernel/univ.ml
index 747a901f45..61ad1d0a82 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -160,13 +160,6 @@ module Level = struct
 
   let compare u v =
     if u == v then 0
-    else
-      let c = Int.compare (hash u) (hash v) in
-	if c == 0 then RawLevel.compare (data u) (data v)
-	else c
-
-  let natural_compare u v =
-    if u == v then 0
     else RawLevel.compare (data u) (data v)
 	    
   let to_string x = 
@@ -954,6 +947,8 @@ struct
   let repr (inst, cst) =
     (Array.mapi (fun i _l -> Level.var i) inst, cst)
 
+  let pr f ?variance ctx = pr f ?variance (repr ctx)
+
   let instantiate inst (u, cst) =
     assert (Array.length u = Array.length inst);
     subst_instance_constraints inst cst
@@ -1054,7 +1049,7 @@ struct
     (univs, cst)
 
   let sort_levels a = 
-    Array.sort Level.natural_compare a; a
+    Array.sort Level.compare a; a
 
   let to_context (ctx, cst) =
     (Instance.of_array (sort_levels (Array.of_list (LSet.elements ctx))), cst)
diff --git a/printing/prettyp.ml b/printing/prettyp.ml
index 9ed985195f..66f748454d 100644
--- a/printing/prettyp.ml
+++ b/printing/prettyp.ml
@@ -71,17 +71,17 @@ 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 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, univs = Global.type_of_global_in_context (Global.env ()) ref in
+  let inst = Univ.make_abstract_instance univs in
+  let bl = UnivNames.universe_binders_with_opt_names ref udecl in
+  let sigma = Evd.from_ctx (UState.of_binders bl) in
   let typ = EConstr.of_constr typ in
   let typ =
     if reduce then
       let env = Global.env () in
-      let sigma = Evd.from_env env in
       let ctx,ccl = Reductionops.splay_prod_assum env sigma typ
       in EConstr.it_mkProd_or_LetIn ccl ctx
     else typ in
-  let univs = Global.universes_of_global ref in
   let variance = match ref with
     | VarRef _ | ConstRef _ -> None
     | IndRef (ind,_) | ConstructRef ((ind,_),_) ->
@@ -91,19 +91,14 @@ let print_ref reduce ref udecl =
         | Declarations.Cumulative_ind cumi -> Some (Univ.ACumulativityInfo.variance cumi)
       end
   in
-  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 = UnivNames.universe_binders_with_opt_names ref
-      (Array.to_list (Univ.Instance.to_array inst)) udecl in
-  let sigma = Evd.from_ctx (UState.of_binders bl) in
   let inst =
     if Global.is_polymorphic ref
-    then Printer.pr_universe_instance sigma (Univ.UContext.instance univs)
+    then Printer.pr_universe_instance sigma inst
     else mt ()
   in
   hov 0 (pr_global ref ++ inst ++ str " :" ++ spc () ++ pr_letype_env env sigma typ ++ 
-           Printer.pr_universe_ctx sigma ?variance univs)
+           Printer.pr_abstract_universe_ctx sigma ?variance univs)
 
 (********************************)
 (** Printing implicit arguments *)
@@ -552,48 +547,31 @@ let print_typed_body env evd (val_0,typ) =
 let print_instance sigma cb =
   if Declareops.constant_is_polymorphic cb then
     let univs = Declareops.constant_polymorphic_context cb in
-    let inst = Univ.AUContext.instance univs in
+    let inst = Univ.make_abstract_instance univs in
     pr_universe_instance sigma inst
   else mt()
 				
 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 =
-    match cb.const_universes with
-    | Monomorphic_const _ -> cb.const_type
-    | Polymorphic_const univs ->
-      let inst = Univ.AUContext.instance univs in
-      Vars.subst_instance_constr inst cb.const_type
-  in
-  let univs, ulist =
-    let open Entries in
+  let typ = cb.const_type in
+  let univs =
     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, []
-        | Polymorphic_const 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
+    | Undef _ | Def _ -> cb.const_universes
     | OpaqueDef o ->
       let body_uctxs = Opaqueproof.force_constraints otab o in
       match cb.const_universes with
       | Monomorphic_const ctx ->
-        Monomorphic_const_entry (ContextSet.union body_uctxs ctx), []
+        Monomorphic_const (ContextSet.union body_uctxs ctx)
       | Polymorphic_const 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)
+        Polymorphic_const ctx
   in
   let ctx =
     UState.of_binders
-      (UnivNames.universe_binders_with_opt_names (ConstRef sp) ulist udecl)
+      (UnivNames.universe_binders_with_opt_names (ConstRef sp) udecl)
   in
   let env = Global.env () and sigma = Evd.from_ctx ctx in
   let pr_ltype = pr_ltype_env env sigma in
@@ -605,7 +583,6 @@ let print_constant with_values sep sp udecl =
 	str" ]" ++
         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_constant_universes sigma univs)
@@ -712,11 +689,6 @@ let print_eval x = !object_pr.print_eval x
 (**** Printing declarations and judgments *)
 (****  Abstract layer                 *****)
 
-let print_typed_value x =
-  let env = Global.env () in
-  let sigma = Evd.from_env env in
-  print_typed_value_in_env env sigma x
-
 let print_judgment env sigma {uj_val=trm;uj_type=typ} =
   print_typed_value_in_env env sigma (trm, typ)
 
@@ -852,11 +824,9 @@ let print_opaque_name env sigma qid =
         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
-	let ty = Vars.subst_instance_constr inst ty in
 	let ty = EConstr.of_constr ty in
         let open EConstr in
-	print_typed_value (mkConstruct cstr, ty)
+        print_typed_value_in_env env sigma (mkConstruct cstr, ty)
     | VarRef id ->
         env |> lookup_named id |> print_named_decl env sigma
 
diff --git a/printing/printer.ml b/printing/printer.ml
index 5ca330d377..3a2450c426 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -270,9 +270,16 @@ let pr_universe_ctx sigma ?variance c =
   else
     mt()
 
+let pr_abstract_universe_ctx sigma ?variance c =
+  if !Detyping.print_universes && not (Univ.AUContext.is_empty c) then
+    fnl()++pr_in_comment (fun c -> v 0
+      (Univ.pr_abstract_universe_context (Termops.pr_evd_level sigma) ?variance c)) 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
+  | Declarations.Monomorphic_const ctx -> pr_universe_ctx_set sigma ctx
+  | Declarations.Polymorphic_const ctx -> pr_abstract_universe_ctx sigma ctx
 
 let pr_cumulativity_info sigma cumi =
   if !Detyping.print_universes 
@@ -282,6 +289,14 @@ let pr_cumulativity_info sigma cumi =
   else
     mt()
 
+let pr_abstract_cumulativity_info sigma cumi =
+  if !Detyping.print_universes
+  && not (Univ.AUContext.is_empty (Univ.ACumulativityInfo.univ_context cumi)) then
+    fnl()++pr_in_comment (fun uii -> v 0
+      (Univ.pr_abstract_cumulativity_info (Termops.pr_evd_level sigma) uii)) cumi
+  else
+    mt()
+
 (**********************************************************************)
 (* Global references *)
 
diff --git a/printing/printer.mli b/printing/printer.mli
index 518c5b930b..96db7091a6 100644
--- a/printing/printer.mli
+++ b/printing/printer.mli
@@ -123,9 +123,12 @@ val pr_cumulative          : bool -> bool -> Pp.t
 val pr_universe_instance   : evar_map -> Univ.Instance.t -> Pp.t
 val pr_universe_ctx        : evar_map -> ?variance:Univ.Variance.t array ->
   Univ.UContext.t -> Pp.t
+val pr_abstract_universe_ctx        : evar_map -> ?variance:Univ.Variance.t array ->
+  Univ.AUContext.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_constant_universes  : evar_map -> Declarations.constant_universes -> Pp.t
 val pr_cumulativity_info   : evar_map -> Univ.CumulativityInfo.t -> Pp.t
+val pr_abstract_cumulativity_info   : evar_map -> Univ.ACumulativityInfo.t -> Pp.t
 
 (** Printing global references using names as short as possible *)
 
diff --git a/printing/printmod.ml b/printing/printmod.ml
index e2d9850bf8..1fc308ac99 100644
--- a/printing/printmod.ml
+++ b/printing/printmod.ml
@@ -90,9 +90,7 @@ let build_ind_type env mip =
   Inductive.type_of_inductive env mip
 
 let print_one_inductive env sigma mib ((_,i) as ind) =
-  let u = if Declareops.inductive_is_polymorphic mib then 
-      Univ.AUContext.instance (Declareops.inductive_polymorphic_context mib)
-    else Univ.Instance.empty in
+  let u = Univ.make_abstract_instance (Declareops.inductive_polymorphic_context mib) in
   let mip = mib.mind_packets.(i) in
   let params = Inductive.inductive_paramdecls (mib,u) in
   let nparamdecls = Context.Rel.length params in
@@ -111,16 +109,6 @@ let print_one_inductive env sigma mib ((_,i) as ind) =
     str ": " ++ Printer.pr_lconstr_env envpar sigma arity ++ str " :=") ++
   brk(0,2) ++ print_constructors envpar sigma mip.mind_consnames cstrtypes
 
-let instantiate_cumulativity_info cumi =
-  let open Univ in
-  let univs = ACumulativityInfo.univ_context cumi in
-  let expose ctx =
-    let inst = AUContext.instance ctx in
-    let cst = AUContext.instantiate inst ctx in
-    UContext.make (inst, cst)
-  in
-  CumulativityInfo.make (expose univs, ACumulativityInfo.variance cumi)
-
 let print_mutual_inductive env mind mib udecl =
   let inds = List.init (Array.length mib.mind_packets) (fun x -> (mind, x))
   in
@@ -131,14 +119,7 @@ let print_mutual_inductive env mind mib udecl =
     | BiFinite -> "Variant"
     | CoFinite -> "CoInductive"
   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 = UnivNames.universe_binders_with_opt_names (IndRef (mind, 0)) univs udecl in
+  let bl = UnivNames.universe_binders_with_opt_names (IndRef (mind, 0)) udecl in
   let sigma = Evd.from_ctx (UState.of_binders bl) in
   hov 0 (Printer.pr_polymorphic (Declareops.inductive_is_polymorphic mib) ++
          Printer.pr_cumulative
@@ -150,8 +131,7 @@ let print_mutual_inductive env mind mib udecl =
          match mib.mind_universes with
          | Monomorphic_ind _ | Polymorphic_ind _ -> str ""
          | Cumulative_ind cumi ->
-           Printer.pr_cumulativity_info
-             sigma (instantiate_cumulativity_info cumi))
+           Printer.pr_abstract_cumulativity_info sigma cumi)
 
 let get_fields =
   let rec prodec_rec l subst c =
@@ -167,11 +147,7 @@ let get_fields =
   prodec_rec [] []
 
 let print_record env mind mib udecl =
-  let u = 
-    if Declareops.inductive_is_polymorphic mib then 
-      Univ.AUContext.instance (Declareops.inductive_polymorphic_context mib)
-    else Univ.Instance.empty 
-  in
+  let u = Univ.make_abstract_instance (Declareops.inductive_polymorphic_context mib) in
   let mip = mib.mind_packets.(0) in
   let params = Inductive.inductive_paramdecls (mib,u) in
   let nparamdecls = Context.Rel.length params in
@@ -181,8 +157,7 @@ let print_record env mind mib udecl =
   let cstrtype = hnf_prod_applist_assum env nparamdecls cstrtypes.(0) args in
   let fields = get_fields cstrtype in
   let envpar = push_rel_context params env in
-  let bl = UnivNames.universe_binders_with_opt_names (IndRef (mind,0))
-      (Array.to_list (Univ.Instance.to_array u)) udecl in
+  let bl = UnivNames.universe_binders_with_opt_names (IndRef (mind,0)) udecl in
   let sigma = Evd.from_ctx (UState.of_binders bl) in
   let keyword =
     let open Declarations in
@@ -210,8 +185,7 @@ let print_record env mind mib udecl =
     match mib.mind_universes with
     | Monomorphic_ind _ | Polymorphic_ind _ -> str ""
     | Cumulative_ind cumi ->
-      Printer.pr_cumulativity_info
-        sigma (instantiate_cumulativity_info cumi)
+      Printer.pr_abstract_cumulativity_info sigma cumi
   )
 
 let pr_mutual_inductive_body env mind mib udecl =
@@ -315,12 +289,6 @@ let print_body is_impl env mp (l,body) =
     | SFBmodtype _ -> keyword "Module Type" ++ spc () ++ name
     | SFBconst cb ->
        let ctx = Declareops.constant_polymorphic_context cb in
-       let u =
-	 if Declareops.constant_is_polymorphic cb then
-            Univ.AUContext.instance ctx
-	 else Univ.Instance.empty
-       in
-       let ctx = Univ.UContext.make (u, Univ.AUContext.instantiate u ctx) in
       (match cb.const_body with
 	| Def _ -> def "Definition" ++ spc ()
 	| OpaqueDef _ when is_impl -> def "Theorem" ++ spc ()
@@ -328,18 +296,17 @@ let print_body is_impl env mp (l,body) =
       (match env with
 	  | None -> mt ()
 	  | Some env ->
+            let bl = UnivNames.universe_binders_with_opt_names (ConstRef (Constant.make2 mp l)) None in
+            let sigma = Evd.from_ctx (UState.of_binders bl) in
 	    str " :" ++ spc () ++
-            hov 0 (Printer.pr_ltype_env env (Evd.from_env env)
-		(Vars.subst_instance_constr u
-   		  cb.const_type)) ++
+            hov 0 (Printer.pr_ltype_env env sigma cb.const_type) ++
 	    (match cb.const_body with
 	      | Def l when is_impl ->
 		spc () ++
 		hov 2 (str ":= " ++
-                       Printer.pr_lconstr_env env (Evd.from_env env)
-			  (Vars.subst_instance_constr u (Mod_subst.force_constr l)))
+                       Printer.pr_lconstr_env env sigma (Mod_subst.force_constr l))
 	      | _ -> mt ()) ++ str "." ++
-            Printer.pr_universe_ctx (Evd.from_env env) ctx)
+            Printer.pr_abstract_universe_ctx sigma ctx)
     | SFBmind mib ->
       try
 	let env = Option.get env in
diff --git a/test-suite/output/UnivBinders.out b/test-suite/output/UnivBinders.out
index 926114a1e1..f8f11d7cf6 100644
--- a/test-suite/output/UnivBinders.out
+++ b/test-suite/output/UnivBinders.out
@@ -86,10 +86,10 @@ Type@{M} -> Type@{N} -> Type@{E}
 (* 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@{u Top.17 v} = 
+Type@{Top.17} -> Type@{v} -> Type@{u}
+     : Type@{max(u+1,Top.17+1,v+1)}
+(* u Top.17 v |=  *)
 
 foo is universe polymorphic
 NonCumulative Inductive Empty@{E} : Type@{E} :=  
@@ -129,11 +129,19 @@ insec@{v} = Type@{u} -> Type@{v}
 (* v |=  *)
 
 insec is universe polymorphic
+NonCumulative Inductive insecind@{k} : Type@{k+1} :=
+    inseccstr : Type@{k} -> insecind@{k}
+
+For inseccstr: Argument scope is [type_scope]
 insec@{u v} = Type@{u} -> Type@{v}
      : Type@{max(u+1,v+1)}
 (* u v |=  *)
 
 insec is universe polymorphic
+NonCumulative Inductive insecind@{u k} : Type@{k+1} :=
+    inseccstr : Type@{k} -> insecind@{u k}
+
+For inseccstr: Argument scope is [type_scope]
 inmod@{u} = Type@{u}
      : Type@{u+1}
 (* u |=  *)
@@ -155,24 +163,24 @@ inmod@{u} -> Type@{v}
 (* u v |=  *)
 
 Applied.infunct is universe polymorphic
-axfoo@{i Top.48 Top.49} : Type@{Top.48} -> Type@{i}
-(* i Top.48 Top.49 |=  *)
+axfoo@{i Top.55 Top.56} : Type@{Top.55} -> Type@{i}
+(* i Top.55 Top.56 |=  *)
 
 axfoo is universe polymorphic
 Argument scope is [type_scope]
 Expands to: Constant Top.axfoo
-axbar@{i Top.48 Top.49} : Type@{Top.49} -> Type@{i}
-(* i Top.48 Top.49 |=  *)
+axbar@{i Top.55 Top.56} : Type@{Top.56} -> Type@{i}
+(* i Top.55 Top.56 |=  *)
 
 axbar is universe polymorphic
 Argument scope is [type_scope]
 Expands to: Constant Top.axbar
-axfoo' : Type@{Top.51} -> Type@{axbar'.i}
+axfoo' : Type@{Top.58} -> Type@{axbar'.i}
 
 axfoo' is not universe polymorphic
 Argument scope is [type_scope]
 Expands to: Constant Top.axfoo'
-axbar' : Type@{Top.51} -> Type@{axbar'.i}
+axbar' : Type@{Top.58} -> Type@{axbar'.i}
 
 axbar' is not universe polymorphic
 Argument scope is [type_scope]
diff --git a/test-suite/output/UnivBinders.v b/test-suite/output/UnivBinders.v
index f806a9f4f7..9aebce1b9a 100644
--- a/test-suite/output/UnivBinders.v
+++ b/test-suite/output/UnivBinders.v
@@ -122,8 +122,12 @@ Section SomeSec.
   Universe u.
   Definition insec@{v} := Type@{u} -> Type@{v}.
   Print insec.
+
+  Inductive insecind@{k} := inseccstr : Type@{k} -> insecind.
+  Print insecind.
 End SomeSec.
 Print insec.
+Print insecind.
 
 Module SomeMod.
   Definition inmod@{u} := Type@{u}.
diff --git a/vernac/himsg.ml b/vernac/himsg.ml
index e7b2a0e8a6..71155d7921 100644
--- a/vernac/himsg.ml
+++ b/vernac/himsg.ml
@@ -896,7 +896,8 @@ let explain_not_match_error = function
       quote (Printer.safe_pr_lconstr_env env (Evd.from_env env) t2)
   | IncompatibleConstraints cst ->
     str " the expected (polymorphic) constraints do not imply " ++
-      let cst = Univ.AUContext.instantiate (Univ.AUContext.instance cst) cst in
+      let cst = Univ.UContext.constraints (Univ.AUContext.repr cst) in
+      (** FIXME: provide a proper naming for the bound variables *)
       quote (Univ.pr_constraints (Termops.pr_evd_level Evd.empty) cst)
 
 let explain_signature_mismatch l spec why =