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.

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 =