diff options
| author | filliatr | 2006-03-01 15:25:17 +0000 |
|---|---|---|
| committer | filliatr | 2006-03-01 15:25:17 +0000 |
| commit | 60dc2f1f6f6b0ec0d9c0826c320e08930f3a4d93 (patch) | |
| tree | d313df7eeed21f3d1cba7b071d722adc9fc25394 /contrib/dp/tests.v | |
| parent | 9222e2ffa0786c870f284f2bcaaf96c551221aa4 (diff) | |
appel de Zenon
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8106 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib/dp/tests.v')
| -rw-r--r-- | contrib/dp/tests.v | 13 |
1 files changed, 5 insertions, 8 deletions
diff --git a/contrib/dp/tests.v b/contrib/dp/tests.v index 222d08cc83..c41a461734 100644 --- a/contrib/dp/tests.v +++ b/contrib/dp/tests.v @@ -5,8 +5,7 @@ Require Import Classical. (* First example with the 0 and the equality translated *) Goal 0 = 0. - -simplify. +zenon. Qed. @@ -16,8 +15,7 @@ Qed. Parameter A C : Prop. Goal A -> A. - -simplify. +zenon. Qed. @@ -37,7 +35,7 @@ Qed. Goal ((((A -> C) -> A) -> A) -> C) -> C. -simplify. +zenon. Qed. @@ -45,7 +43,6 @@ Qed. Open Scope Z_scope. Goal 1 + 1 = 2. - simplify. Qed. @@ -58,8 +55,8 @@ Qed. (* Universal quantifier *) -Goal (forall (x y : Z), x = y) -> 0 = 1. - +Goal (forall (x y : Z), x = y) -> 0=1. +zenon. simplify. Qed. |