aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7>2010-05-02 15:23:34 +0000
committerGravatar msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7>2010-05-02 15:23:34 +0000
commitdecc15b1012171310047e92643087ae0d7289823 (patch)
tree0c444b550e4520a7911166c406546a9570b47625
parent2ac0d62e7765e26d9538918cbf582046a97932c7 (diff)
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
-rw-r--r--tactics/btermdn.ml3
-rw-r--r--tactics/nbtermdn.ml2
-rw-r--r--tactics/nbtermdn.mli2
-rw-r--r--tactics/termdn.ml12
-rw-r--r--tactics/termdn.mli2
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