Imported Upstream version 8.2~rc2+dfsgupstream/8.2.rc2+dfsg

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 *)