No more Univ in grammar.cma

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15385 85f007b7-540e-0410-9357-904b9bb8a0f7

6 files changed, 11 insertions, 8 deletions

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 38fe7a1ca..7537e7d0b 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -65,7 +65,7 @@ let print_implicits_defensive = ref true
 let print_coercions = ref false
 
 (* This forces printing universe names of Type{.} *)
-let print_universes = ref false
+let print_universes = Detyping.print_universes
 
 (* This suppresses printing of primitive tokens (e.g. numeral) and symbols *)
 let print_no_symbol = ref false
diff --git a/intf/misctypes.mli b/intf/misctypes.mli
index 2aec5ed32..a51145812 100644
--- a/intf/misctypes.mli
+++ b/intf/misctypes.mli
@@ -37,7 +37,8 @@ type 'id move_location =
 
 (** Sorts *)
 
-type glob_sort = GProp | GSet | GType of Univ.universe option
+type sort_info = Pp.std_ppcmds option
+type glob_sort = GProp | GSet | GType of sort_info
 
 (** Casts *)
 
diff --git a/parsing/grammar.mllib b/parsing/grammar.mllib
index 27ca281c8..c99ae47d0 100644
--- a/parsing/grammar.mllib
+++ b/parsing/grammar.mllib
@@ -16,8 +16,6 @@ Predicate
 Option
 
 Names
-Univ
-
 Libnames
 Summary
 Genarg
diff --git a/parsing/ppconstr.ml b/parsing/ppconstr.ml
index f08ef361d..b64dd6ff8 100644
--- a/parsing/ppconstr.ml
+++ b/parsing/ppconstr.ml
@@ -112,12 +112,10 @@ let pr_sep_com sep f c = pr_with_comments (constr_loc c) (sep() ++ f c)
 
 let pr_in_comment pr x = str "(* " ++ pr x ++ str " *)"
 
-let pr_universe = Univ.pr_uni
-
 let pr_glob_sort = function
   | GProp -> str "Prop"
   | GSet -> str "Set"
-  | GType u -> hov 0 (str "Type" ++ pr_opt (pr_in_comment pr_universe) u)
+  | GType u -> hov 0 (str "Type" ++ pr_opt (pr_in_comment (fun x->x)) u)
 
 let pr_id = pr_id
 let pr_name = pr_name
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index ab4388047..fd20f199c 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -32,6 +32,9 @@ open Decl_kinds
 
 let dl = dummy_loc
 
+(** Should we keep details of universes during detyping ? *)
+let print_universes = ref false
+
 (****************************************************************************)
 (* Tools for printing of Cases                                              *)
 
@@ -367,7 +370,7 @@ let detype_case computable detype detype_eqns testdep avoid data p c bl =
 let detype_sort = function
   | Prop Null -> GProp
   | Prop Pos -> GSet
-  | Type u -> GType (Some u)
+  | Type u -> GType (if !print_universes then Some (Univ.pr_uni u) else None)
 
 type binder_kind = BProd | BLambda | BLetIn
 
diff --git a/pretyping/detyping.mli b/pretyping/detyping.mli
index 439609b02..10f23b1b2 100644
--- a/pretyping/detyping.mli
+++ b/pretyping/detyping.mli
@@ -17,6 +17,9 @@ open Termops
 open Mod_subst
 open Misctypes
 
+(** Should we keep details of universes during detyping ? *)
+val print_universes : bool ref
+
 val subst_cases_pattern : substitution -> cases_pattern -> cases_pattern
 
 val subst_glob_constr : substitution -> glob_constr -> glob_constr