- coqc : option -image

- coqmktop : manquaient des -I
- tauto : rétablissement du vieux tauto en attendant la stabilité du nouveau
- correction d'un bug de Simpl avec Fix (découvert dans preuve FTA)


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

6 files changed, 10 insertions, 9 deletions

diff --git a/theories/Bool/Bool.v b/theories/Bool/Bool.v
index f546a1aa1..7826e3882 100755
--- a/theories/Bool/Bool.v
+++ b/theories/Bool/Bool.v
@@ -326,7 +326,7 @@ Hints Resolve andb_true_intro : bool v62.
 Lemma andb_true_intro2 : 
   (b1,b2:bool)(Is_true b1)->(Is_true b2)->(Is_true (andb b1 b2)).
 Proof.
-  Destruct b1; Destruct b2; Tauto.
+  Destruct b1; Destruct b2; Simpl; Tauto.
 Save.
 Hints Resolve andb_true_intro2 : bool v62.
 
diff --git a/theories/Lists/ListSet.v b/theories/Lists/ListSet.v
index a1c86e78f..3c083aa97 100644
--- a/theories/Lists/ListSet.v
+++ b/theories/Lists/ListSet.v
@@ -189,7 +189,7 @@ Section first_definitions.
     Simpl; Intros [H1|H2]; Auto with datatypes.
     Simpl; Do 3 Intro.
     Elim (Aeq_dec b a0).
-    Tauto.
+    Simpl; Tauto.
     Simpl; Intros; Elim H0.
     Trivial with datatypes.
     Tauto.
@@ -271,7 +271,7 @@ Section first_definitions.
     (set_In a (set_inter x y)) -> (set_In a y).
   Proof.
     Induction x.
-    Tauto.
+    Simpl; Tauto.
     Simpl; Intros a0 l Hrec y.
     Generalize (!set_mem_correct1 a0 y).
     Elim (set_mem a0 y); Simpl; Intros.
@@ -291,7 +291,7 @@ Section first_definitions.
     (set_In a x) -> ~(set_In a y) -> (set_In a (set_diff x y)).
   Proof.
     Induction x.
-    Tauto.
+    Simpl; Tauto.
     Simpl; Intros a0 l Hrec y [Ha0a | Hal] Hay.
     Rewrite Ha0a; Generalize (set_mem_complete2 Hay).
     Elim (set_mem a y); [ Intro Habs; Discriminate Habs | Auto with datatypes ].
@@ -302,7 +302,7 @@ Section first_definitions.
     (set_In a (set_diff x y)) -> (set_In a x).
   Proof.
     Induction x.
-    Tauto.
+    Simpl; Tauto.
     Simpl; Intros a0 l Hrec y; Elim (set_mem a0 y).
     EAuto with datatypes.
     Intro; Generalize (set_add_elim  H).
diff --git a/theories/Lists/PolyList.v b/theories/Lists/PolyList.v
index 6477d9f0c..1a0211d54 100644
--- a/theories/Lists/PolyList.v
+++ b/theories/Lists/PolyList.v
@@ -561,7 +561,7 @@ Save.
 Lemma in_prod : (A:Set)(B:Set)(l:(list A))(l':(list B))
   (x:A)(y:B)(In x l)->(In y l')->(In (x,y) (list_prod l l')).
 Induction l;
-[ Tauto
+[ Simpl; Intros; Tauto
 | Simpl; Intros; Apply in_or_app; Elim H0; Clear H0;
   [ Left; Rewrite H0; Apply in_prod_aux; Assumption
   | Right; Auto]
diff --git a/theories/Sets/Partial_Order.v b/theories/Sets/Partial_Order.v
index 7b0f432ba..a1c1639f0 100755
--- a/theories/Sets/Partial_Order.v
+++ b/theories/Sets/Partial_Order.v
@@ -87,6 +87,7 @@ Qed.
 Lemma Strict_Rel_Transitive: (Transitive U (Strict_Rel_of U D)).
 Red.
 Intros x y z H' H'0.
-Apply Strict_Rel_Transitive_with_Rel with y := y; Intuition.
+Apply Strict_Rel_Transitive_with_Rel with y := y; 
+  [ Intuition | Unfold Strict_Rel_of in H' H'0; Intuition ].
 Qed.
 End Partial_order_facts.
diff --git a/theories/Sets/Relations_1_facts.v b/theories/Sets/Relations_1_facts.v
index ad6b55c0c..3c9609182 100755
--- a/theories/Sets/Relations_1_facts.v
+++ b/theories/Sets/Relations_1_facts.v
@@ -72,7 +72,7 @@ Theorem cong_reflexive_same_relation:
   (U:Type) (R, R':(Relation U)) (same_relation U R R') -> (Reflexive U R) ->
   (Reflexive U R').
 Proof.
-Intuition.
+Unfold same_relation; Intuition.
 Qed.
 
 Theorem cong_symmetric_same_relation:
diff --git a/theories/Zarith/auxiliary.v b/theories/Zarith/auxiliary.v
index e7bcdcfab..0b69cd236 100644
--- a/theories/Zarith/auxiliary.v
+++ b/theories/Zarith/auxiliary.v
@@ -210,7 +210,7 @@ Theorem not_or : (A,B:Prop) ~(A\/B) -> ~A /\ ~B.
 Tauto. Save.
 
 Theorem not_and : (A,B:Prop) (decidable A) -> ~(A/\B) -> ~A \/ ~B.
-Tauto. Save.
+Unfold decidable; Tauto. Save.
 
 Theorem not_imp : (A,B:Prop) (decidable A) -> ~(A -> B) -> A /\ ~B.
 Unfold decidable;Tauto.