From 4c28e0597067d81f5ee7e8b2b2e668f4d45e973f Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 12 Sep 2018 11:42:32 +0200
Subject: Fix printing of abstract universe contexts.

Due to their representation using names, the instance was not properly
displayed.
---
 kernel/univ.ml | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/kernel/univ.ml b/kernel/univ.ml
index 311477daca..8acbeb2d25 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -954,6 +954,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
-- 
cgit v1.2.3


From 51dad02266f0bea735d496839c559b472bc4553e Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 11 Sep 2018 11:00:42 +0200
Subject: Removing calls to AUContext.instance.

We simply declare the bound universes with their user-facing name in the
evarmap and call all printing functions on uninstantiated terms. We had to
tweak the universe name declaring function so that it would work properly
with bound universe variables and handle sections correctly.

This changes the output of polymorphic definitions with unnamed universe
variables. Now they are printed as Var(i) instead of the Module.n uid
that came from their absolute name.
---
 engine/univNames.ml               | 33 +++++++++++++++++++++++++
 printing/prettyp.ml               | 51 ++++++++++++---------------------------
 printing/printer.ml               | 19 +++++++++++++--
 printing/printer.mli              |  5 +++-
 printing/printmod.ml              | 46 +++++++++--------------------------
 test-suite/output/UnivBinders.out | 26 ++++++++++----------
 vernac/himsg.ml                   |  3 ++-
 7 files changed, 96 insertions(+), 87 deletions(-)

diff --git a/engine/univNames.ml b/engine/univNames.ml
index e861913de2..29d92c46ea 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
@@ -65,6 +66,24 @@ let subst_ubinder (subst,(ref,l as orig)) =
   if ref == ref' then orig else ref', l
 
 let discharge_ubinder (_,(ref,l)) =
+  (** Expand polymorphic binders with the section context *)
+  let info = Lib.section_segment_of_reference ref in
+  let sec_inst = info.Lib.abstr_subst in
+  let shift = Instance.length sec_inst in
+  let map lvl = match Level.var_index lvl with
+  | None -> lvl
+  | Some n -> Level.var (n + shift)
+  in
+  let l = Id.Map.map map l in
+  let fold i accu lvl = match Level.name lvl with
+  | None -> accu
+  | Some na ->
+    try
+      let qid = Nametab.shortest_qualid_of_universe na in
+      Id.Map.add (snd (Libnames.repr_qualid qid)) (Level.var i) accu
+    with Not_found -> accu
+  in
+  let l = Array.fold_left_i fold l (Instance.to_array sec_inst) in
   Some (Lib.discharge_global ref, l)
 
 let ubinder_obj : GlobRef.t * universe_binders -> Libobject.obj =
@@ -86,6 +105,20 @@ let register_universe_binders ref ubinders =
     else ubinders)
     !universe_map ubinders
   in
+  let ubinders =
+    if Global.is_polymorphic ref then
+      (** FIXME: little dance to make the named universes refer to bound
+          universe variables *)
+      let univs = AUContext.instance (Global.universes_of_global ref) in
+      let fold i accu l = LMap.add l i accu in
+      let univs = Array.fold_left_i fold LMap.empty (Instance.to_array univs) in
+      let fold id lvl accu =
+        try Id.Map.add id (Level.var (LMap.find lvl univs)) accu
+        with Not_found -> accu
+      in
+      Id.Map.fold fold ubinders Id.Map.empty
+    else ubinders
+  in
   if not (Id.Map.is_empty ubinders)
   then Lib.add_anonymous_leaf (ubinder_obj (ref,ubinders))
 
diff --git a/printing/prettyp.ml b/printing/prettyp.ml
index 9ed985195f..605c1ae957 100644
--- a/printing/prettyp.ml
+++ b/printing/prettyp.ml
@@ -71,17 +71,18 @@ 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
+      (Array.to_list (Univ.Instance.to_array inst)) 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 +92,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,43 +548,36 @@ 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 typ = cb.const_type in
   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 ctx, []
         | Polymorphic_const ctx ->
-          let inst = AUContext.instance ctx in
-          Polymorphic_const_entry (UContext.make (inst, AUContext.instantiate inst ctx)),
+          let inst = make_abstract_instance ctx in
+          Polymorphic_const 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 (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)),
+        let inst = make_abstract_instance ctx in
+        Polymorphic_const ctx,
         Array.to_list (Instance.to_array inst)
   in
   let ctx =
@@ -605,7 +594,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 +700,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 +835,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 5b3ead181f..043371be73 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 971241d5f9..f977ab2372 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..f8d88aea07 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
@@ -135,7 +123,7 @@ let print_mutual_inductive env mind mib udecl =
     let open Univ in
     if Declareops.inductive_is_polymorphic mib then
       Array.to_list (Instance.to_array
-                       (AUContext.instance (Declareops.inductive_polymorphic_context mib)))
+                       (make_abstract_instance (Declareops.inductive_polymorphic_context mib)))
     else []
   in
   let bl = UnivNames.universe_binders_with_opt_names (IndRef (mind, 0)) univs udecl in
@@ -150,8 +138,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 +154,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
@@ -210,8 +193,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 +297,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 +304,18 @@ let print_body is_impl env mp (l,body) =
       (match env with
 	  | None -> mt ()
 	  | Some env ->
+            let univs = Array.to_list (Univ.Instance.to_array (Univ.make_abstract_instance ctx)) in
+            let bl = UnivNames.universe_binders_with_opt_names (ConstRef (Constant.make2 mp l)) univs 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..22b998fab9 100644
--- a/test-suite/output/UnivBinders.out
+++ b/test-suite/output/UnivBinders.out
@@ -42,10 +42,10 @@ bar@{u} = nat
          *)
 
 bar is universe polymorphic
-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@{u Var(1) v} = 
+Type@{Var(1)} -> Type@{v} -> Type@{u}
+     : Type@{max(u+1,Var(1)+1,v+1)}
+(* u Var(1) v |=  *)
 
 foo is universe polymorphic
 Type@{i} -> Type@{j}
@@ -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@{Var(0) Var(1) Var(2)} = 
+Type@{Var(1)} -> Type@{Var(2)} -> Type@{Var(0)}
+     : Type@{max(Var(0)+1,Var(1)+1,Var(2)+1)}
+(* Var(0) Var(1) Var(2) |=  *)
 
 foo is universe polymorphic
 NonCumulative Inductive Empty@{E} : Type@{E} :=  
@@ -125,7 +125,7 @@ bind_univs.poly@{u} = Type@{u}
 
 bind_univs.poly is universe polymorphic
 insec@{v} = Type@{u} -> Type@{v}
-     : Type@{max(u+1,v+1)}
+     : Type@{max(v+1,u+1)}
 (* v |=  *)
 
 insec is universe polymorphic
@@ -155,14 +155,14 @@ 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 Var(1) Var(2)} : Type@{Var(1)} -> Type@{i}
+(* i Var(1) Var(2) |=  *)
 
 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 Var(1) Var(2)} : Type@{Var(2)} -> Type@{i}
+(* i Var(1) Var(2) |=  *)
 
 axbar is universe polymorphic
 Argument scope is [type_scope]
diff --git a/vernac/himsg.ml b/vernac/himsg.ml
index a4650cfd92..1b6d12a976 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 =
-- 
cgit v1.2.3


From aaee23f06e4ac345238cb84edc1c16fafe6b6b3d Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 13 Sep 2018 13:47:13 +0200
Subject: Store universe binder names as a mere list of names.

This is the only information we care about. The printing mechanism is only
called on polymorphic constants, as the naming of global monomorphic levels
is performed in another module.
---
 engine/univNames.ml  | 87 +++++++++++++++++++++++-----------------------------
 engine/univNames.mli | 11 +++----
 engine/universes.ml  |  1 -
 engine/universes.mli |  4 +--
 printing/prettyp.ml  | 23 ++++----------
 printing/printmod.ml | 15 ++-------
 6 files changed, 53 insertions(+), 88 deletions(-)

diff --git a/engine/univNames.ml b/engine/univNames.ml
index 29d92c46ea..a4a08ff18e 100644
--- a/engine/univNames.ml
+++ b/engine/univNames.ml
@@ -53,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 : Name.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
@@ -68,25 +68,19 @@ let subst_ubinder (subst,(ref,l as orig)) =
 let discharge_ubinder (_,(ref,l)) =
   (** Expand polymorphic binders with the section context *)
   let info = Lib.section_segment_of_reference ref in
-  let sec_inst = info.Lib.abstr_subst in
-  let shift = Instance.length sec_inst in
-  let map lvl = match Level.var_index lvl with
-  | None -> lvl
-  | Some n -> Level.var (n + shift)
-  in
-  let l = Id.Map.map map l in
-  let fold i accu lvl = match Level.name lvl with
-  | None -> accu
+  let sec_inst = Array.to_list (Instance.to_array (info.Lib.abstr_subst)) in
+  let map i lvl = match Level.name lvl with
+  | None -> Anonymous
   | Some na ->
     try
       let qid = Nametab.shortest_qualid_of_universe na in
-      Id.Map.add (snd (Libnames.repr_qualid qid)) (Level.var i) accu
-    with Not_found -> accu
+      Name (snd (Libnames.repr_qualid qid))
+    with Not_found -> Anonymous
   in
-  let l = Array.fold_left_i fold l (Instance.to_array sec_inst) in
+  let l = List.mapi 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 * Name.t list -> Libobject.obj =
   let open Libobject in
   declare_object { (default_object "universe binder") with
     cache_function = cache_ubinder;
@@ -97,42 +91,37 @@ 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
-  in
-  let ubinders =
-    if Global.is_polymorphic ref then
-      (** FIXME: little dance to make the named universes refer to bound
-          universe variables *)
-      let univs = AUContext.instance (Global.universes_of_global ref) in
-      let fold i accu l = LMap.add l i accu in
-      let univs = Array.fold_left_i fold LMap.empty (Instance.to_array univs) in
-      let fold id lvl accu =
-        try Id.Map.add id (Level.var (LMap.find lvl univs)) accu
-        with Not_found -> accu
-      in
-      Id.Map.fold fold ubinders Id.Map.empty
-    else 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 Name (LMap.find lvl revmap)
+    with Not_found -> Anonymous
   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
+let universe_binders_with_opt_names ref names =
+  let udecl = match names with
   | None -> universe_binders_of_global ref
-  | 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
-      CErrors.user_err ~hdr:"universe_binders_with_opt_names"
-        Pp.(str "Universe instance should have length " ++ int (List.length levels))
+  | Some udecl -> List.map (fun na -> na.CAst.v) udecl
+  in
+  let () =
+    try
+      let ctx = Global.universes_of_global ref in
+      let len = AUContext.size ctx in
+      if not (Option.is_empty names || Int.equal len (List.length udecl)) then
+        CErrors.user_err ~hdr:"universe_binders_with_opt_names"
+          Pp.(str "Universe instance should have length " ++ int len)
+    with Not_found -> ()
+  in
+  let fold i acc = function
+  | Anonymous -> acc
+  | Name 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/printing/prettyp.ml b/printing/prettyp.ml
index 605c1ae957..66f748454d 100644
--- a/printing/prettyp.ml
+++ b/printing/prettyp.ml
@@ -73,8 +73,7 @@ let print_basename sp = pr_global (ConstRef sp)
 let print_ref reduce ref udecl =
   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
-      (Array.to_list (Univ.Instance.to_array inst)) udecl 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 =
@@ -556,33 +555,23 @@ 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 = cb.const_type in
-  let univs, ulist =
+  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 ctx, []
-        | Polymorphic_const ctx ->
-          let inst = make_abstract_instance ctx in
-          Polymorphic_const 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 (ContextSet.union body_uctxs ctx), []
+        Monomorphic_const (ContextSet.union body_uctxs ctx)
       | Polymorphic_const ctx ->
         assert(ContextSet.is_empty body_uctxs);
-        let inst = make_abstract_instance ctx in
-        Polymorphic_const 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
diff --git a/printing/printmod.ml b/printing/printmod.ml
index f8d88aea07..1fc308ac99 100644
--- a/printing/printmod.ml
+++ b/printing/printmod.ml
@@ -119,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
-                       (make_abstract_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
@@ -164,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
@@ -304,8 +296,7 @@ let print_body is_impl env mp (l,body) =
       (match env with
 	  | None -> mt ()
 	  | Some env ->
-            let univs = Array.to_list (Univ.Instance.to_array (Univ.make_abstract_instance ctx)) in
-            let bl = UnivNames.universe_binders_with_opt_names (ConstRef (Constant.make2 mp l)) univs None in
+            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 sigma cb.const_type) ++
-- 
cgit v1.2.3


From 138f7c628e546775b381fa1f8805acc433839684 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 13 Sep 2018 15:14:01 +0200
Subject: Best-effort hack to provide a meaningful name for anonymous bound
 universes.

This restores the old behaviour that was printing qualified global names as
a representation of anonymous bound universes, at the cost of a ugly hack.
Ideally this should be handled by the callers, but for the time being the
trade-off is probably OK.
---
 engine/univNames.ml               |  9 +++++++--
 test-suite/output/UnivBinders.out | 16 ++++++++--------
 2 files changed, 15 insertions(+), 10 deletions(-)

diff --git a/engine/univNames.ml b/engine/univNames.ml
index a4a08ff18e..bdcad21a21 100644
--- a/engine/univNames.ml
+++ b/engine/univNames.ml
@@ -65,6 +65,11 @@ 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. *)
+  try Name (Id.of_string_soft (Level.to_string lvl)) with _ -> Anonymous
+
 let discharge_ubinder (_,(ref,l)) =
   (** Expand polymorphic binders with the section context *)
   let info = Lib.section_segment_of_reference ref in
@@ -75,7 +80,7 @@ let discharge_ubinder (_,(ref,l)) =
     try
       let qid = Nametab.shortest_qualid_of_universe na in
       Name (snd (Libnames.repr_qualid qid))
-    with Not_found -> Anonymous
+    with Not_found -> name_universe lvl
   in
   let l = List.mapi map sec_inst @ l in
   Some (Lib.discharge_global ref, l)
@@ -99,7 +104,7 @@ let register_universe_binders ref ubinders =
   let revmap = Id.Map.fold (fun id lvl accu -> LMap.add lvl id accu) ubinders LMap.empty in
   let map lvl =
     try Name (LMap.find lvl revmap)
-    with Not_found -> Anonymous
+    with Not_found -> name_universe lvl
   in
   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))
diff --git a/test-suite/output/UnivBinders.out b/test-suite/output/UnivBinders.out
index 22b998fab9..0f673acb79 100644
--- a/test-suite/output/UnivBinders.out
+++ b/test-suite/output/UnivBinders.out
@@ -42,10 +42,10 @@ bar@{u} = nat
          *)
 
 bar is universe polymorphic
-foo@{u Var(1) v} = 
-Type@{Var(1)} -> Type@{v} -> Type@{u}
-     : Type@{max(u+1,Var(1)+1,v+1)}
-(* u Var(1) v |=  *)
+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
 Type@{i} -> Type@{j}
@@ -155,14 +155,14 @@ inmod@{u} -> Type@{v}
 (* u v |=  *)
 
 Applied.infunct is universe polymorphic
-axfoo@{i Var(1) Var(2)} : Type@{Var(1)} -> Type@{i}
-(* i Var(1) Var(2) |=  *)
+axfoo@{i Top.48 Top.49} : Type@{Top.48} -> Type@{i}
+(* i Top.48 Top.49 |=  *)
 
 axfoo is universe polymorphic
 Argument scope is [type_scope]
 Expands to: Constant Top.axfoo
-axbar@{i Var(1) Var(2)} : Type@{Var(2)} -> Type@{i}
-(* i Var(1) Var(2) |=  *)
+axbar@{i Top.48 Top.49} : Type@{Top.49} -> Type@{i}
+(* i Top.48 Top.49 |=  *)
 
 axbar is universe polymorphic
 Argument scope is [type_scope]
-- 
cgit v1.2.3


From 0d7643dabade293696a377dbc1f858dff2d666f4 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Fri, 14 Sep 2018 13:35:47 +0200
Subject: Universe binders are Id, not Name. Never print Var.

Comes with minor cleanups in exception catching and unnecessary mapi.
---
 doc/sphinx/proof-engine/vernacular-commands.rst |  4 +-
 engine/univNames.ml                             | 51 ++++++++++++-------------
 test-suite/output/UnivBinders.out               |  8 ++--
 3 files changed, 31 insertions(+), 32 deletions(-)

diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst
index 56df535d85..1e17a773a6 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 bdcad21a21..9e4c6e47fc 100644
--- a/engine/univNames.ml
+++ b/engine/univNames.ml
@@ -53,7 +53,7 @@ let empty_binders = Id.Map.empty
 
 let universe_binders_table = Summary.ref GlobRef.Map.empty ~name:"universe binders"
 
-let universe_binders_of_global ref : Name.t list =
+let universe_binders_of_global ref : Id.t list =
   try
     let l = GlobRef.Map.find ref !universe_binders_table in l
   with Not_found -> []
@@ -68,24 +68,25 @@ let subst_ubinder (subst,(ref,l as orig)) =
 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. *)
-  try Name (Id.of_string_soft (Level.to_string lvl)) with _ -> Anonymous
+  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 i lvl = match Level.name lvl with
-  | None -> Anonymous
-  | Some na ->
-    try
-      let qid = Nametab.shortest_qualid_of_universe na in
-      Name (snd (Libnames.repr_qualid qid))
-    with Not_found -> name_universe lvl
+  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.mapi map sec_inst @ l in
+  let l = List.map map sec_inst @ l in
   Some (Lib.discharge_global ref, l)
 
-let ubinder_obj : GlobRef.t * Name.t list -> 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;
@@ -103,7 +104,7 @@ let register_universe_binders ref ubinders =
   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 Name (LMap.find lvl revmap)
+    try LMap.find lvl revmap
     with Not_found -> name_universe lvl
   in
   let ubinders = Array.map_to_list map (Instance.to_array univs) in
@@ -112,21 +113,19 @@ let register_universe_binders ref ubinders =
 type univ_name_list = Names.lname list
 
 let universe_binders_with_opt_names ref names =
+  let orig = universe_binders_of_global ref in
   let udecl = match names with
-  | None -> universe_binders_of_global ref
-  | Some udecl -> List.map (fun na -> na.CAst.v) udecl
-  in
-  let () =
+  | None -> orig
+  | Some udecl ->
     try
-      let ctx = Global.universes_of_global ref in
-      let len = AUContext.size ctx in
-      if not (Option.is_empty names || Int.equal len (List.length udecl)) then
-        CErrors.user_err ~hdr:"universe_binders_with_opt_names"
-          Pp.(str "Universe instance should have length " ++ int len)
-    with Not_found -> ()
-  in
-  let fold i acc = function
-  | Anonymous -> acc
-  | Name na -> Names.Id.Map.add na (Level.var i) acc
+      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 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/test-suite/output/UnivBinders.out b/test-suite/output/UnivBinders.out
index 0f673acb79..75276c7d0e 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@{Var(0) Var(1) Var(2)} = 
-Type@{Var(1)} -> Type@{Var(2)} -> Type@{Var(0)}
-     : Type@{max(Var(0)+1,Var(1)+1,Var(2)+1)}
-(* Var(0) Var(1) Var(2) |=  *)
+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} :=  
-- 
cgit v1.2.3


From 4cbbbf0842eab2a996f749957c2e5120d91d6faf Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Fri, 14 Sep 2018 13:38:44 +0200
Subject: Add test for univ names of polymorphic inductives in sections.

This used to print Var (before #8475, even with explicit binders) but
now doesn't.
---
 test-suite/output/UnivBinders.out | 20 ++++++++++++++------
 test-suite/output/UnivBinders.v   |  4 ++++
 2 files changed, 18 insertions(+), 6 deletions(-)

diff --git a/test-suite/output/UnivBinders.out b/test-suite/output/UnivBinders.out
index 75276c7d0e..01eff57299 100644
--- a/test-suite/output/UnivBinders.out
+++ b/test-suite/output/UnivBinders.out
@@ -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}.
-- 
cgit v1.2.3


From 7d4d30ab00ded50e4c15c1b078044ea10dfb2fc1 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Wed, 19 Sep 2018 23:07:00 +0200
Subject: Remove hash based univ level compare

---
 kernel/univ.ml                    | 9 +--------
 test-suite/output/UnivBinders.out | 2 +-
 2 files changed, 2 insertions(+), 9 deletions(-)

diff --git a/kernel/univ.ml b/kernel/univ.ml
index 8acbeb2d25..3e1f8f2cab 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -159,13 +159,6 @@ module Level = struct
     | _ -> false
 
   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)
 	    
@@ -1056,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/test-suite/output/UnivBinders.out b/test-suite/output/UnivBinders.out
index 01eff57299..f8f11d7cf6 100644
--- a/test-suite/output/UnivBinders.out
+++ b/test-suite/output/UnivBinders.out
@@ -125,7 +125,7 @@ bind_univs.poly@{u} = Type@{u}
 
 bind_univs.poly is universe polymorphic
 insec@{v} = Type@{u} -> Type@{v}
-     : Type@{max(v+1,u+1)}
+     : Type@{max(u+1,v+1)}
 (* v |=  *)
 
 insec is universe polymorphic
-- 
cgit v1.2.3