diff options
author | Stephane Glondu <steph@glondu.net> | 2010-07-21 09:46:51 +0200 |
---|---|---|
committer | Stephane Glondu <steph@glondu.net> | 2010-07-21 09:46:51 +0200 |
commit | 5b7eafd0f00a16d78f99a27f5c7d5a0de77dc7e6 (patch) | |
tree | 631ad791a7685edafeb1fb2e8faeedc8379318ae /test-suite/modules/PO.v | |
parent | da178a880e3ace820b41d38b191d3785b82991f5 (diff) |
Imported Upstream snapshot 8.3~beta0+13298
Diffstat (limited to 'test-suite/modules/PO.v')
-rw-r--r-- | test-suite/modules/PO.v | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/test-suite/modules/PO.v b/test-suite/modules/PO.v index 354c3957..71d33177 100644 --- a/test-suite/modules/PO.v +++ b/test-suite/modules/PO.v @@ -7,11 +7,11 @@ Implicit Arguments snd. Module Type PO. Parameter T : Set. Parameter le : T -> T -> Prop. - + Axiom le_refl : forall x : T, le x x. Axiom le_trans : forall x y z : T, le x y -> le y z -> le x z. Axiom le_antis : forall x y : T, le x y -> le y x -> x = y. - + Hint Resolve le_refl le_trans le_antis. End PO. @@ -28,10 +28,10 @@ Module Pair (X: PO) (Y: PO) <: PO. Lemma le_trans : forall p1 p2 p3 : T, le p1 p2 -> le p2 p3 -> le p1 p3. unfold le in |- *; intuition; info eauto. - Qed. + Qed. Lemma le_antis : forall p1 p2 : T, le p1 p2 -> le p2 p1 -> p1 = p2. - destruct p1. + destruct p1. destruct p2. unfold le in |- *. intuition. |