diff options
| author | filliatr | 2006-02-28 15:36:03 +0000 |
|---|---|---|
| committer | filliatr | 2006-02-28 15:36:03 +0000 |
| commit | 30392d5cb910fae96eee91ae30cebfb864be41db (patch) | |
| tree | f4731c27f2bec000d74685a482325c293ca4dbca /contrib/dp/tests.v | |
| parent | fd7be7fc9fec071d76b9ce7671f754f20e02790a (diff) | |
*** empty log message ***
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8103 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib/dp/tests.v')
| -rw-r--r-- | contrib/dp/tests.v | 14 |
1 files changed, 7 insertions, 7 deletions
diff --git a/contrib/dp/tests.v b/contrib/dp/tests.v index 10b6f0d835..222d08cc83 100644 --- a/contrib/dp/tests.v +++ b/contrib/dp/tests.v @@ -1,4 +1,3 @@ -Reset Initial. Require Import ZArith. Require Import Classical. @@ -64,10 +63,11 @@ Goal (forall (x y : Z), x = y) -> 0 = 1. simplify. Qed. +Goal forall (x: nat), (x + 0 = x)%nat. -Goal forall (x y : Z), x + y = y + x. - -induction x ; simplify. +induction x0. +zenon. +zenon. Qed. @@ -98,7 +98,7 @@ simplify. Qed. -(* Inductive types definitions - call to injection function *) +(* Inductive types definitions - call to incontrib/dp/jection function *) Inductive even : Z -> Prop := | even_0 : even 0 @@ -185,9 +185,9 @@ Qed. (* sorts issues *) Parameter foo : Set. -Parameter f : nat -> foo -> foo -> nat. +Parameter ff : nat -> foo -> foo -> nat. Parameter g : foo -> foo. -Goal (forall x:foo, f 0 x x = O) -> forall y, f 0 (g y) (g y) = O. +Goal (forall x:foo, ff 0 x x = O) -> forall y, ff 0 (g y) (g y) = O. simplify. Qed. |