Fix bug 2958: Inductive deep in in clause are impossible

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

1 files changed, 22 insertions, 0 deletions

diff --git a/test-suite/success/CaseInClause.v b/test-suite/success/CaseInClause.v
new file mode 100644
index 000000000..3679eead7
--- /dev/null
+++ b/test-suite/success/CaseInClause.v
@@ -0,0 +1,22 @@
+(* in clause pattern *)
+Require Vector.
+Check (fun n (x: Vector.t True (S n)) =>
+  match x in Vector.t _ (S m) return True with
+    |Vector.cons _ h _ _ => h
+  end).
+
+(* Notation *)
+Import Vector.VectorNotations.
+Notation "A \dots n" := (Vector.t A n) (at level 200).
+Check (fun m (x: Vector.t nat m) =>
+  match x in _ \dots k return Vector.t nat (S k) with
+    | Vector.nil _ => 0 :: []
+    | Vector.cons _ h _ t => h :: h :: t
+  end).
+
+(* N should be a variable and not the inductiveRef *)
+Require Import NArith.
+Theorem foo : forall (n m : nat) (pf : n = m),
+                match pf in _ = N with 
+                  | eq_refl => unit
+                end.