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.