Work on dep types pattern matching

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

1 files changed, 13 insertions, 0 deletions

diff --git a/contrib/subtac/test/euclid.v b/contrib/subtac/test/euclid.v
index 39fdc9ba7..55e5e9035 100644
--- a/contrib/subtac/test/euclid.v
+++ b/contrib/subtac/test/euclid.v
@@ -1,3 +1,16 @@
+Print eq_rec.
+Print eq.
+Inductive vector : nat -> Set :=
+  | vnil : vector 0
+  | vcons : nat -> forall n, vector n -> vector (S n).
+Set Printing All.
+Print eq.
+Program Fixpoint vapp (n m : nat) (v : vector n) (w : vector m) { struct v } : vector (n + m) :=
+  match v with
+  | vnil => w
+  | vcons a n' v' => vcons a (n' + m) (vapp n' m v' w)
+  end.
+
 
 Notation "( x & y )" := (@existS _ _ x y) : core_scope.
 Unset Printing All.