- Another bug in get_sort_family_of (sort-polymorphism of constants and

  inductive types was not taken into account).
- Virtually extended tauto to 
  - support arbitrary-length disjunctions and conjunctions,
  - support arbitrary complex forms of disjunctions and
    conjunctions when in the contravariant of an implicative hypothesis,
  - stick with the purely propositional fragment and not apply reflexivity.
  This is virtual in the sense that it is not activated since it breaks 
  compatibility with the existing tauto.
- Modified the notion of conjunction and unit type used in hipattern in a 
  way that is closer to the intuitive meaning (forbid dependencies 
  between parameters in conjunction; forbid indices in unit types).
- Investigated how far "iff" could be turned into a direct inductive
  definition; modified tauto.ml4 so that it works with the current and
  the alternative definition.
- Fixed a bug in the error message from lookup_eliminator.
- Other minor changes.



git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11721 85f007b7-540e-0410-9357-904b9bb8a0f7

2 files changed, 10 insertions, 12 deletions

diff --git a/theories/Init/Logic.v b/theories/Init/Logic.v
index b01b80630b..a91fd0480b 100644
--- a/theories/Init/Logic.v
+++ b/theories/Init/Logic.v
@@ -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] *)
 
diff --git a/theories/Init/Tactics.v b/theories/Init/Tactics.v
index 0e8b4ab1f0..2e0fe42b68 100644
--- a/theories/Init/Tactics.v
+++ b/theories/Init/Tactics.v
@@ -139,18 +139,6 @@ bapply lemma ltac:(fun H => destruct H as [_ H]; apply H in J).
     proofs "in one step" *)
 
 Ltac easy :=
-(*
-  let rec use_hyp H :=
-    match type of H with
-    | _ /\ _ => 
-    | _ => solve [inversion H] 
-    end
-  with destruct_hyp H :=
-    match type of H with
-    | _ /\ _ => case H; do_intro; do_intro
-    | _ => idtac
-    end
-*)
   let rec use_hyp H :=
     match type of H with
     | _ /\ _ => exact H || destruct_hyp H