summaryrefslogtreecommitdiff
path: root/test-suite/success/CasesDep.v
diff options
context:
space:
mode:
authorGravatar Stephane Glondu <steph@glondu.net>2012-01-12 16:04:54 +0100
committerGravatar Stephane Glondu <steph@glondu.net>2012-01-12 16:04:54 +0100
commit39efc41237ec906226a3a53d7396d51173495204 (patch)
tree87cd58d72d43469d2a2a0a127c1060d7c9e0206b /test-suite/success/CasesDep.v
parent5fe4ac437bed43547b3695664974f492b55cb553 (diff)
parent97fefe1fcca363a1317e066e7f4b99b9c1e9987b (diff)
Remove non-DFSG contentsupstream/8.4_beta+dfsg
Diffstat (limited to 'test-suite/success/CasesDep.v')
-rw-r--r--test-suite/success/CasesDep.v54
1 files changed, 54 insertions, 0 deletions
diff --git a/test-suite/success/CasesDep.v b/test-suite/success/CasesDep.v
index 29721843..d3b7cf3f 100644
--- a/test-suite/success/CasesDep.v
+++ b/test-suite/success/CasesDep.v
@@ -26,6 +26,40 @@ Fixpoint foldrn (n : nat) (bs : listn B n) {struct bs} : C :=
end.
End Folding.
+(** Testing post-processing of nested dependencies *)
+
+Check fun x:{x|x=0}*nat+nat => match x with
+ | inl ((exist 0 eq_refl),0) => None
+ | _ => Some 0
+ end.
+
+Check fun x:{_:{x|x=0}|True}+nat => match x with
+ | inl (exist (exist 0 eq_refl) I) => None
+ | _ => Some 0
+ end.
+
+Check fun x:{_:{x|x=0}|True}+nat => match x with
+ | inl (exist (exist 0 eq_refl) I) => None
+ | _ => Some 0
+ end.
+
+Check fun x:{_:{x|x=0}|True}+nat => match x return option nat with
+ | inl (exist (exist 0 eq_refl) I) => None
+ | _ => Some 0
+ end.
+
+ (* the next two examples were failing from r14703 (Nov 22 2011) to r14732 *)
+ (* due to a bug in dependencies postprocessing (revealed by CoLoR) *)
+
+Check fun x:{x:nat*nat|fst x = 0 & True} => match x return option nat with
+ | exist2 (x,y) eq_refl I => None
+ end.
+
+Check fun x:{_:{x:nat*nat|fst x = 0 & True}|True}+nat => match x return option nat with
+ | inl (exist (exist2 (x,y) eq_refl I) I) => None
+ | _ => Some 0
+ end.
+
(* -------------------------------------------------------------------- *)
(* Example to test patterns matching on dependent families *)
(* This exemple extracted from the developement done by Nacira Chabane *)
@@ -506,3 +540,23 @@ Definition test (s:step E E) :=
| Step nil _ (cons E nil) _ Plus l l' => true
| _ => false
end.
+
+(* Testing regression of bug 2454 ("get" used not be type-checkable when
+ defined with its type constraint) *)
+
+Inductive K : nat -> Type := KC : forall (p q:nat), K p.
+
+Definition get : K O -> nat := fun x => match x with KC p q => q end.
+
+(* Checking correct order of substitution of realargs *)
+(* (was broken from revision 14664 to 14669) *)
+(* Example extracted from contrib CoLoR *)
+
+Inductive EQ : nat -> nat -> Prop := R x y : EQ x y.
+
+Check fun e t (d1 d2:EQ e t) =>
+ match d1 in EQ e1 t1, d2 in EQ e2 t2 return
+ (e1,t1) = (e2,t2) -> (e1,t1) = (e,t) -> 0=0
+ with
+ | R _ _, R _ _ => fun _ _ => eq_refl
+ end.