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.

1 files changed, 33 insertions, 0 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))