Univs: proper printing of global and local universe names (only

printing functions touched in the kernel).

6 files changed, 40 insertions, 28 deletions

diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 2df197546..046ee0dad 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -394,18 +394,13 @@ let detype_case computable detype detype_eqns testdep avoid data p c bl =
       let eqnl = detype_eqns constructs constagsl bl in
       GCases (dl,tag,pred,[tomatch,(alias,aliastyp)],eqnl)
 
-let detype_sort = function
+let detype_sort sigma = function
   | Prop Null -> GProp
   | Prop Pos -> GSet
   | Type u ->
     GType
       (if !print_universes
-       then 
-	  let _, map = Universes.global_universe_names () in
-	  let pr_level u = 
-	    try Nameops.pr_id (Univ.LMap.find u map) with Not_found -> Univ.Level.pr u
-	  in 
-	    [Pp.string_of_ppcmds (Univ.Universe.pr_with pr_level u)]
+       then [Pp.string_of_ppcmds (Univ.Universe.pr_with (Evd.pr_evd_level sigma) u)]
        else [])
 
 type binder_kind = BProd | BLambda | BLetIn
@@ -416,12 +411,12 @@ type binder_kind = BProd | BLambda | BLetIn
 let detype_anonymous = ref (fun loc n -> anomaly ~label:"detype" (Pp.str "index to an anonymous variable"))
 let set_detype_anonymous f = detype_anonymous := f
 
-let detype_level l =
-  GType (Some (Pp.string_of_ppcmds (Univ.Level.pr l)))
+let detype_level sigma l =
+  GType (Some (Pp.string_of_ppcmds (Evd.pr_evd_level sigma l)))
 
-let detype_instance l = 
+let detype_instance sigma l = 
   if Univ.Instance.is_empty l then None
-  else Some (List.map detype_level (Array.to_list (Univ.Instance.to_array l)))
+  else Some (List.map (detype_level sigma) (Array.to_list (Univ.Instance.to_array l)))
 
 let rec detype flags avoid env sigma t =
   match kind_of_term (collapse_appl t) with
@@ -439,7 +434,7 @@ let rec detype flags avoid env sigma t =
     | Var id ->
 	(try let _ = Global.lookup_named id in GRef (dl, VarRef id, None)
 	 with Not_found -> GVar (dl, id))
-    | Sort s -> GSort (dl,detype_sort s)
+    | Sort s -> GSort (dl,detype_sort sigma s)
     | Cast (c1,REVERTcast,c2) when not !Flags.raw_print ->
         detype flags avoid env sigma c1
     | Cast (c1,k,c2) ->
@@ -463,7 +458,7 @@ let rec detype flags avoid env sigma t =
       in
 	mkapp (detype flags avoid env sigma f)
 	  (Array.map_to_list (detype flags avoid env sigma) args)
-    | Const (sp,u) -> GRef (dl, ConstRef sp, detype_instance u)
+    | Const (sp,u) -> GRef (dl, ConstRef sp, detype_instance sigma u)
     | Proj (p,c) ->
       let noparams () = 
 	let pb = Environ.lookup_projection p (snd env) in
@@ -521,9 +516,9 @@ let rec detype flags avoid env sigma t =
         GEvar (dl,id,
                List.map (on_snd (detype flags avoid env sigma)) l)
     | Ind (ind_sp,u) ->
-	GRef (dl, IndRef ind_sp, detype_instance u)
+	GRef (dl, IndRef ind_sp, detype_instance sigma u)
     | Construct (cstr_sp,u) ->
-	GRef (dl, ConstructRef cstr_sp, detype_instance u)
+	GRef (dl, ConstructRef cstr_sp, detype_instance sigma u)
     | Case (ci,p,c,bl) ->
 	let comp = computable p (List.length (ci.ci_pp_info.ind_tags)) in
 	detype_case comp (detype flags avoid env sigma)
diff --git a/pretyping/detyping.mli b/pretyping/detyping.mli
index 725fff5b2..eb158686a 100644
--- a/pretyping/detyping.mli
+++ b/pretyping/detyping.mli
@@ -43,7 +43,7 @@ val detype_case :
   Id.t list -> inductive * case_style * bool list array * bool list ->
     constr option -> constr -> constr array -> glob_constr
 
-val detype_sort : sorts -> glob_sort
+val detype_sort : evar_map -> sorts -> glob_sort
 
 val detype_rel_context : ?lax:bool -> constr option -> Id.t list -> (names_context * env) -> 
   evar_map -> rel_context -> glob_decl list
diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index d629fd5f5..ee72d3147 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -275,7 +275,7 @@ end
 
 (* 2nd part used to check consistency on the fly. *)
 type evar_universe_context = 
- { uctx_names : Univ.Level.t UNameMap.t;
+ { uctx_names : Univ.Level.t UNameMap.t * string Univ.LMap.t;
    uctx_local : Univ.universe_context_set; (** The local context of variables *)
     uctx_univ_variables : Universes.universe_opt_subst;
       (** The local universes that are unification variables *)
@@ -288,7 +288,7 @@ type evar_universe_context =
   }
   
 let empty_evar_universe_context = 
-  { uctx_names = UNameMap.empty;
+  { uctx_names = UNameMap.empty, Univ.LMap.empty;
     uctx_local = Univ.ContextSet.empty;
     uctx_univ_variables = Univ.LMap.empty;
     uctx_univ_algebraic = Univ.LSet.empty;
@@ -309,8 +309,9 @@ let union_evar_universe_context ctx ctx' =
   else if is_empty_evar_universe_context ctx' then ctx
   else
     let local = Univ.ContextSet.union ctx.uctx_local ctx'.uctx_local in
-    let names = UNameMap.union ctx.uctx_names ctx'.uctx_names in
-      { uctx_names = names;
+    let names = UNameMap.union (fst ctx.uctx_names) (fst ctx'.uctx_names) in
+    let names_rev = Univ.LMap.union (snd ctx.uctx_names) (snd ctx'.uctx_names) in
+      { uctx_names = (names, names_rev);
 	uctx_local = local;
 	uctx_univ_variables = 
 	  Univ.LMap.subst_union ctx.uctx_univ_variables ctx'.uctx_univ_variables;
@@ -1004,6 +1005,9 @@ let merge_universe_subst evd subst =
 let with_context_set rigid d (a, ctx) = 
   (merge_context_set rigid d ctx, a)
 
+let add_uctx_names s l (names, names_rev) =
+    (UNameMap.add s l names, Univ.LMap.add l s names_rev)
+
 let uctx_new_univ_variable rigid name
   ({ uctx_local = ctx; uctx_univ_variables = uvars; uctx_univ_algebraic = avars} as uctx) =
   let u = Universes.new_univ_level (Global.current_dirpath ()) in
@@ -1018,7 +1022,7 @@ let uctx_new_univ_variable rigid name
 	else {uctx with uctx_univ_variables = Univ.LMap.add u None uvars} in
   let names = 
     match name with
-    | Some n -> UNameMap.add n u uctx.uctx_names
+    | Some n -> add_uctx_names n u uctx.uctx_names
     | None -> uctx.uctx_names
   in
     {uctx' with uctx_names = names; uctx_local = ctx';
@@ -1253,11 +1257,10 @@ let nf_constraints =
   else nf_constraints
 
 let universe_of_name evd s = 
-  UNameMap.find s evd.universes.uctx_names
+  UNameMap.find s (fst evd.universes.uctx_names)
 
 let add_universe_name evd s l =
-  let names = evd.universes.uctx_names in
-  let names' = UNameMap.add s l names in
+  let names' = add_uctx_names s l evd.universes.uctx_names in
     {evd with universes = {evd.universes with uctx_names = names'}}
 
 let universes evd = evd.universes.uctx_universes
@@ -1689,11 +1692,23 @@ let evar_dependency_closure n sigma =
 let has_no_evar sigma =
   EvMap.is_empty sigma.defn_evars && EvMap.is_empty sigma.undf_evars
 
+let pr_uctx_level uctx = 
+  let map, map_rev = uctx.uctx_names in 
+    fun l ->
+      try str(Univ.LMap.find l map_rev)
+      with Not_found -> 
+	Universes.pr_with_global_universes l
+
+let pr_evd_level evd = pr_uctx_level evd.universes
+
 let pr_evar_universe_context ctx =
+  let prl = pr_uctx_level ctx in
   if is_empty_evar_universe_context ctx then mt ()
   else
-    (str"UNIVERSES:"++brk(0,1)++ h 0 (Univ.pr_universe_context_set ctx.uctx_local) ++ fnl () ++
-     str"ALGEBRAIC UNIVERSES:"++brk(0,1)++h 0 (Univ.LSet.pr ctx.uctx_univ_algebraic) ++ fnl() ++
+    (str"UNIVERSES:"++brk(0,1)++ 
+       h 0 (Univ.pr_universe_context_set prl ctx.uctx_local) ++ fnl () ++
+     str"ALGEBRAIC UNIVERSES:"++brk(0,1)++
+     h 0 (Univ.LSet.pr prl ctx.uctx_univ_algebraic) ++ fnl() ++
      str"UNDEFINED UNIVERSES:"++brk(0,1)++
        h 0 (Universes.pr_universe_opt_subst ctx.uctx_univ_variables) ++ fnl())
 
diff --git a/pretyping/evd.mli b/pretyping/evd.mli
index 82daa7da3..53f8b0db8 100644
--- a/pretyping/evd.mli
+++ b/pretyping/evd.mli
@@ -598,6 +598,7 @@ val pr_evar_map_filter : ?with_univs:bool -> (Evar.t -> evar_info -> bool) ->
   evar_map -> Pp.std_ppcmds
 val pr_metaset : Metaset.t -> Pp.std_ppcmds
 val pr_evar_universe_context : evar_universe_context -> Pp.std_ppcmds
+val pr_evd_level : evar_map -> Univ.Level.t -> Pp.std_ppcmds
 
 (** {5 Deprecated functions} *)
 
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index b8e3b3b14..a23963abc 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -306,7 +306,8 @@ struct
       match c with
       | Cst_const (c, u) ->
 	if Univ.Instance.is_empty u then Constant.print c
-	else str"(" ++ Constant.print c ++ str ", " ++ Univ.Instance.pr u ++ str")"
+	else str"(" ++ Constant.print c ++ str ", " ++ 
+	  Univ.Instance.pr Univ.Level.pr u ++ str")"
       | Cst_proj p ->
 	str".(" ++ Constant.print (Projection.constant p) ++ str")"
 
diff --git a/pretyping/termops.ml b/pretyping/termops.ml
index eee94f228..5862a8525 100644
--- a/pretyping/termops.ml
+++ b/pretyping/termops.ml
@@ -46,7 +46,7 @@ let pr_fix pr_constr ((t,i),(lna,tl,bl)) =
 
 let pr_puniverses p u = 
   if Univ.Instance.is_empty u then p 
-  else p ++ str"(*" ++ Univ.Instance.pr u ++ str"*)"
+  else p ++ str"(*" ++ Univ.Instance.pr Universes.pr_with_global_universes u ++ str"*)"
 
 let rec pr_constr c = match kind_of_term c with
   | Rel n -> str "#"++int n