Facilites pour le debogguage des univers.

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

5 files changed, 6 insertions, 6 deletions

diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 170de079b7..9ce397dd44 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -291,7 +291,7 @@ let rec detype avoid env t =
     | IsMeta n -> RMeta (dummy_loc, n)
     | IsVar id -> RVar (dummy_loc, id)
     | IsSort (Prop c) -> RSort (dummy_loc,RProp c)
-    | IsSort (Type _) -> RSort (dummy_loc,RType)
+    | IsSort (Type u) -> RSort (dummy_loc,RType (Some u))
     | IsCast (c1,c2) ->
 	RCast(dummy_loc,detype avoid env c1,detype avoid env c2)
     | IsProd (na,ty,c) -> detype_binder BProd avoid env na ty c
diff --git a/pretyping/pattern.ml b/pretyping/pattern.ml
index 01ccd27fa3..f423777d9b 100644
--- a/pretyping/pattern.ml
+++ b/pretyping/pattern.ml
@@ -171,7 +171,7 @@ let matches_core convert pat c =
 
       | PSort (RProp c1), IsSort (Prop c2) when c1 = c2 -> sigma
 
-      | PSort RType, IsSort (Type _) -> sigma
+      | PSort (RType _), IsSort (Type _) -> sigma
 
       | PApp (c1,arg1), IsApp (c2,arg2) ->
         (try array_fold_left2 (sorec stk) (sorec stk sigma c1 c2) arg1 arg2
@@ -309,7 +309,7 @@ let rec pattern_of_constr t =
     | IsMeta n -> PMeta (Some n)
     | IsVar id -> PVar id
     | IsSort (Prop c) -> PSort (RProp c)
-    | IsSort (Type _) -> PSort RType
+    | IsSort (Type _) -> PSort (RType None)
     | IsCast (c,_)      -> pattern_of_constr c
     | IsLetIn (na,c,_,b) -> PLetIn (na,pattern_of_constr c,pattern_of_constr b)
     | IsProd (na,c,b)   -> PProd (na,pattern_of_constr c,pattern_of_constr b)
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index d2855a64ff..9fd30dfc86 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -194,7 +194,7 @@ let pretype_ref _ isevars env lvar ref =
 *)
 let pretype_sort = function
   | RProp c -> judge_of_prop_contents c
-  | RType ->
+  | RType _ ->
       { uj_val = dummy_sort;
 	uj_type = dummy_sort }
 
diff --git a/pretyping/rawterm.ml b/pretyping/rawterm.ml
index e7b5bd5efe..053c6c39b7 100644
--- a/pretyping/rawterm.ml
+++ b/pretyping/rawterm.ml
@@ -26,7 +26,7 @@ type cases_pattern =
   | PatCstr of
       loc * (constructor_path * identifier list) * cases_pattern list * name
 
-type rawsort = RProp of Term.contents | RType
+type rawsort = RProp of Term.contents | RType of Univ.universe option
 
 type binder_kind = BProd | BLambda | BLetIn
 
diff --git a/pretyping/rawterm.mli b/pretyping/rawterm.mli
index 18e3b1a1f4..0106fc60ab 100644
--- a/pretyping/rawterm.mli
+++ b/pretyping/rawterm.mli
@@ -25,7 +25,7 @@ type cases_pattern =
   | PatCstr of
       loc * (constructor_path * identifier list) * cases_pattern list * name
 
-type rawsort = RProp of Term.contents | RType
+type rawsort = RProp of Term.contents | RType of Univ.universe option
 
 type binder_kind = BProd | BLambda | BLetIn