Fix discrimination of sorts which doesn't play well with cumulativity

and type inference putting every new type in some Type universes (bug
reported by L. Pottier).


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

5 files changed, 7 insertions, 14 deletions

diff --git a/tactics/btermdn.ml b/tactics/btermdn.ml
index 13027fd34..ba6586fe0 100644
--- a/tactics/btermdn.ml
+++ b/tactics/btermdn.ml
@@ -77,8 +77,7 @@ struct
       | Var id when not (Idpred.mem id idpred) -> Dn.Label(Term_dn.GRLabel (VarRef id),l)
       | Prod (n, d, c) -> Dn.Label(Term_dn.ProdLabel, [d; c])
       | Lambda (n, d, c) -> Dn.Label(Term_dn.LambdaLabel, [d; c] @ l)
-      | Sort s when is_small s -> Dn.Label(Term_dn.SortLabel (Some s), [])
-      | Sort _ -> Dn.Label(Term_dn.SortLabel None, [])
+      | Sort _ -> Dn.Label(Term_dn.SortLabel, [])
       | Evar _ -> Dn.Everything
       | _ -> Dn.Nothing
 
diff --git a/tactics/nbtermdn.ml b/tactics/nbtermdn.ml
index 67b396dda..f2a60e7d5 100644
--- a/tactics/nbtermdn.ml
+++ b/tactics/nbtermdn.ml
@@ -115,7 +115,7 @@ let constr_val_discr_st (idpred,cpred) t =
     | Var id when not (Idpred.mem id idpred) -> Dn.Label(Term_dn.GRLabel (VarRef id),l)
     | Prod (n, d, c) -> Dn.Label(Term_dn.ProdLabel, [d; c])
     | Lambda (n, d, c) -> Dn.Label(Term_dn.LambdaLabel, [d; c] @ l)
-    | Sort s -> Dn.Label(Term_dn.SortLabel (Some s), [])
+    | Sort _ -> Dn.Label(Term_dn.SortLabel, [])
     | Evar _ -> Dn.Everything
     | _ -> Dn.Nothing
 
diff --git a/tactics/nbtermdn.mli b/tactics/nbtermdn.mli
index 5d80d847e..1dae56052 100644
--- a/tactics/nbtermdn.mli
+++ b/tactics/nbtermdn.mli
@@ -20,7 +20,7 @@ sig
       | GRLabel of global_reference
       | ProdLabel 
       | LambdaLabel
-      | SortLabel of sorts option
+      | SortLabel
   end 
     
   type 'na t
diff --git a/tactics/termdn.ml b/tactics/termdn.ml
index fe5dc572d..9aee3e2ea 100644
--- a/tactics/termdn.ml
+++ b/tactics/termdn.ml
@@ -31,7 +31,7 @@ struct
     | GRLabel of global_reference
     | ProdLabel 
     | LambdaLabel
-    | SortLabel of sorts option
+    | SortLabel
 	
   module Y =  struct 
      type t = term_label
@@ -95,12 +95,7 @@ let constr_pat_discr_st (idpred,cpred) t =
       Some (GRLabel ref, args)
   | PProd (_, d, c), [] -> Some (ProdLabel, [d ; c])
   | PLambda (_, d, c), l -> Some (LambdaLabel, [d ; c] @ l)
-  | PSort s, [] -> 
-      let s' = match s with
-	| RProp c -> Some (Prop c)
-	| RType _ -> None 
-	    (* Don't try to be clever about type levels here *)
-      in Some (SortLabel s', [])
+  | PSort s, [] -> Some (SortLabel, [])
   | _ -> None
 
 open Dn
@@ -123,8 +118,7 @@ let constr_val_discr_st (idpred,cpred) t =
     | Var id when not (Idpred.mem id idpred) -> Label(GRLabel (VarRef id),l)
     | Prod (n, d, c) -> Label(ProdLabel, [d; c])
     | Lambda (n, d, c) -> Label(LambdaLabel, [d; c] @ l)
-    | Sort s when is_small s -> Label(SortLabel (Some s), [])
-    | Sort _ -> Label (SortLabel None, [])
+    | Sort _ -> Label (SortLabel, [])
     | Evar _ -> Everything
     | _ -> Nothing
 
diff --git a/tactics/termdn.mli b/tactics/termdn.mli
index dae4e8e30..1453fdadb 100644
--- a/tactics/termdn.mli
+++ b/tactics/termdn.mli
@@ -54,7 +54,7 @@ sig
     | GRLabel of global_reference
     | ProdLabel 
     | LambdaLabel
-    | SortLabel of sorts option
+    | SortLabel
 	
   val constr_pat_discr_st : transparent_state ->
     constr_pattern -> (term_label * constr_pattern list) option