diff options
| author | msozeau | 2006-11-29 15:34:13 +0000 |
|---|---|---|
| committer | msozeau | 2006-11-29 15:34:13 +0000 |
| commit | 5085103ca30872a3afcb58f85517080c91ec6191 (patch) | |
| tree | 9af09d5178e7b20597537b45070e9359226050ba /contrib/subtac/test | |
| parent | aa552d9b8ba40f641ad1375b07b6f76e34d88fff (diff) | |
Fork of cases impl for subtac.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9407 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib/subtac/test')
| -rw-r--r-- | contrib/subtac/test/euclid.v | 14 |
1 files changed, 0 insertions, 14 deletions
diff --git a/contrib/subtac/test/euclid.v b/contrib/subtac/test/euclid.v index 55e5e90352..8fedeed516 100644 --- a/contrib/subtac/test/euclid.v +++ b/contrib/subtac/test/euclid.v @@ -1,17 +1,3 @@ -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. Require Import Coq.Arith.Compare_dec. |