summaryrefslogtreecommitdiff
path: root/theories/Init/Logic.v
diff options
context:
space:
mode:
authorGravatar Stephane Glondu <steph@glondu.net>2009-02-01 00:54:40 +0100
committerGravatar Stephane Glondu <steph@glondu.net>2009-02-01 00:54:40 +0100
commitcfbfe13f5b515ae2e3c6cdd97e2ccee03bc26e56 (patch)
treeb7832bd5d412a5a5d69cb36ae2ded62c71124c22 /theories/Init/Logic.v
parent113b703a695acbe31ac6dd6a8c4aa94f6fda7545 (diff)
Imported Upstream version 8.2~rc2+dfsgupstream/8.2.rc2+dfsg
Diffstat (limited to 'theories/Init/Logic.v')
-rw-r--r--theories/Init/Logic.v18
1 files changed, 14 insertions, 4 deletions
diff --git a/theories/Init/Logic.v b/theories/Init/Logic.v
index 6a636ccc..ae79744f 100644
--- a/theories/Init/Logic.v
+++ b/theories/Init/Logic.v
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: Logic.v 10304 2007-11-08 17:06:32Z emakarov $ i*)
+(*i $Id: Logic.v 11735 2009-01-02 17:22:31Z herbelin $ i*)
Set Implicit Arguments.
@@ -150,6 +150,16 @@ Proof.
intros; tauto.
Qed.
+Lemma iff_and : forall A B : Prop, (A <-> B) -> (A -> B) /\ (B -> A).
+Proof.
+intros A B []; split; trivial.
+Qed.
+
+Lemma iff_to_and : forall A B : Prop, (A <-> B) <-> (A -> B) /\ (B -> A).
+Proof.
+intros; tauto.
+Qed.
+
(** [(IF_then_else P Q R)], written [IF P then Q else R] denotes
either [P] and [Q], or [~P] and [Q] *)
@@ -245,8 +255,8 @@ Implicit Arguments eq_ind [A].
Implicit Arguments eq_rec [A].
Implicit Arguments eq_rect [A].
-Hint Resolve I conj or_introl or_intror refl_equal: core v62.
-Hint Resolve ex_intro ex_intro2: core v62.
+Hint Resolve I conj or_introl or_intror refl_equal: core.
+Hint Resolve ex_intro ex_intro2: core.
Section Logic_lemmas.
@@ -339,7 +349,7 @@ Proof.
destruct 1; destruct 1; destruct 1; destruct 1; destruct 1; reflexivity.
Qed.
-Hint Immediate sym_eq sym_not_eq: core v62.
+Hint Immediate sym_eq sym_not_eq: core.
(** Basic definitions about relations and properties *)