Facilites pour le debogguage des univers.

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

4 files changed, 18 insertions, 4 deletions

diff --git a/parsing/astterm.ml b/parsing/astterm.ml
index 37725ab7b..85bd1a3e5 100644
--- a/parsing/astterm.ml
+++ b/parsing/astterm.ml
@@ -483,7 +483,7 @@ let ast_to_rawconstr sigma env allow_soapp lvar =
 
     | Node(loc,"PROP", []) -> RSort(loc,RProp Null)
     | Node(loc,"SET", [])  -> RSort(loc,RProp Pos)
-    | Node(loc,"TYPE", []) -> RSort(loc,RType)
+    | Node(loc,"TYPE", _) -> RSort(loc,RType None)
 	  
     (* This case mainly parses things build in a quotation *)
     | Node(loc,("CONST"|"EVAR"|"MUTIND"|"MUTCONSTRUCT"|"SYNCONST" as key),l) ->
@@ -706,7 +706,7 @@ let interp_type_with_implicits sigma env impls c =
 let interp_sort = function
   | Node(loc,"PROP", []) -> Prop Null
   | Node(loc,"SET", [])  -> Prop Pos
-  | Node(loc,"TYPE", []) -> Type Univ.dummy_univ
+  | Node(loc,"TYPE", _) -> Type Univ.dummy_univ
   | a -> user_err_loc (Ast.loc a,"interp_sort", [< 'sTR "Not a sort" >])
 
 let judgment_of_rawconstr sigma env c =
diff --git a/parsing/g_basevernac.ml4 b/parsing/g_basevernac.ml4
index f4edcd544..f3d066f2f 100644
--- a/parsing/g_basevernac.ml4
+++ b/parsing/g_basevernac.ml4
@@ -106,6 +106,12 @@ GEXTEND Gram
       | IDENT "Print"; "Grammar"; uni = identarg; ent = identarg ->
           <:ast< (PrintGrammar $uni $ent) >>
 
+      (* Dump of the universe graph - to file or to stdout *) 
+      | IDENT "Dump"; IDENT "Universes"; f = stringarg ->
+	  <:ast< (DumpUniverses $f) >>
+      | IDENT "Dump"; IDENT "Universes" ->
+	  <:ast< (DumpUniverses) >>
+
       | IDENT "Locate"; IDENT "File"; f = stringarg ->
 	  <:ast< (LocateFile $f) >>
       | IDENT "Locate"; IDENT "Library"; id = identarg ->
diff --git a/parsing/termast.ml b/parsing/termast.ml
index 18ef4b3ac..448aa148a 100644
--- a/parsing/termast.ml
+++ b/parsing/termast.ml
@@ -49,6 +49,10 @@ let print_implicits_explicit_args = ref false
 (* This forces printing of coercions *)
 let print_coercions = ref false
 
+(* This forces printing universe names of Type{.} *)
+let print_universes = ref false
+
+
 let with_option o f x =
   let old = !o in o:=true;
   try let r = f x in o := old; r
@@ -58,6 +62,7 @@ let with_arguments f = with_option print_arguments f
 let with_casts f = with_option print_casts f
 let with_implicits f = with_option print_implicits f
 let with_coercions f = with_option print_coercions f
+let with_universes f = with_option print_universes f
 
 (**********************************************************************)
 (* conversion of references                                           *)
@@ -261,7 +266,8 @@ let rec ast_of_raw = function
       (match s with
 	 | RProp Null -> ope("PROP",[])
 	 | RProp Pos -> ope("SET",[])
-	 | RType -> ope("TYPE",[]))
+	 | RType (Some u) when !print_universes -> ope("TYPE",[ide(Univ.string_of_univ u)])
+	 | RType _ -> ope("TYPE",[]))
   | RHole _ -> ope("ISEVAR",[])
   | RCast (_,c,t) -> ope("CAST",[ast_of_raw c;ast_of_raw t])
 	
@@ -389,7 +395,7 @@ let rec ast_of_pattern env = function
       (match s with
 	 | RProp Null -> ope("PROP",[])
 	 | RProp Pos -> ope("SET",[])
-	 | RType -> ope("TYPE",[]))
+	 | RType _ -> ope("TYPE",[]))
 
   | PMeta (Some n) -> ope("META",[num n])
   | PMeta None -> ope("ISEVAR",[])
diff --git a/parsing/termast.mli b/parsing/termast.mli
index df18bc27e..31dd7d25c 100644
--- a/parsing/termast.mli
+++ b/parsing/termast.mli
@@ -42,8 +42,10 @@ val print_casts : bool ref
 val print_arguments : bool ref
 val print_evar_arguments : bool ref
 val print_coercions : bool ref
+val print_universes : bool ref
 
 val with_casts : ('a -> 'b) -> 'a -> 'b
 val with_implicits : ('a -> 'b) -> 'a -> 'b
 val with_arguments : ('a -> 'b) -> 'a -> 'b
 val with_coercions : ('a -> 'b) -> 'a -> 'b
+val with_universes : ('a -> 'b) -> 'a -> 'b