Imported Upstream version 8.2~beta3+dfsgupstream/8.2.beta3+dfsg

1 files changed, 29 insertions, 0 deletions

diff --git a/test-suite/output/Cases.v b/test-suite/output/Cases.v
index 452d3603..61f89d40 100644
--- a/test-suite/output/Cases.v
+++ b/test-suite/output/Cases.v
@@ -4,3 +4,32 @@ Inductive t : Set :=
     k : let x := t in x -> x.
 
 Print t_rect.
+
+(* Do not contract nested patterns with dependent return type *)
+(* see bug #1699 *)
+
+Require Import Arith.
+
+Definition proj (x y:nat) (P:nat -> Type) (def:P x) (prf:P y) : P y :=
+  match eq_nat_dec x y return P y with
+  | left eqprf => 
+    match eqprf in (_ = z) return (P z) with
+    | refl_equal => def
+    end
+  | _ => prf
+ end.
+
+Print proj.
+
+(* Use notations even below aliases *)
+
+Require Import List.
+
+Fixpoint foo (A:Type) (l:list A) : option A :=
+  match l with
+  | nil => None
+  | x0 :: nil => Some x0
+  | x0 :: (x1 :: xs) as l0 => foo A l0
+  end.
+
+Print foo.