Suppression d'Intuition (trop intelligent?)

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

2 files changed, 6 insertions, 3 deletions

diff --git a/theories/Sets/Finite_sets_facts.v b/theories/Sets/Finite_sets_facts.v
index da50904c5..b19fba44a 100755
--- a/theories/Sets/Finite_sets_facts.v
+++ b/theories/Sets/Finite_sets_facts.v
@@ -189,7 +189,7 @@ Clear H'.
 Intro H'; Red in H'.
 Elim H'; Intros H'0 H'1; Red in H'0; Clear H' H'1.
 Absurd (In U (Add U X0 x0) x); Auto with sets.
-LApply (Add_inv U X0 x0 x); Intuition.
+LApply (Add_inv U X0 x0 x); [ Intuition | Apply (H'0 x); Apply Add_intro2 ].
 Qed.
 
 Lemma cardinal_Empty : (m:nat)(cardinal U (Empty_set U) m) -> O = m.
diff --git a/theories/Sets/Relations_1_facts.v b/theories/Sets/Relations_1_facts.v
index c86e57318..ad6b55c0c 100755
--- a/theories/Sets/Relations_1_facts.v
+++ b/theories/Sets/Relations_1_facts.v
@@ -79,13 +79,16 @@ Theorem cong_symmetric_same_relation:
   (U:Type) (R, R':(Relation U)) (same_relation U R R') -> (Symmetric U R) ->
   (Symmetric U R').
 Proof.
-Intuition.
+  Compute;Intros;Elim H;Intros;Clear H;Apply (H3 y x (H0 x y (H2 x y H1))).
+(*Intuition.*)
 Qed.
 
 Theorem cong_antisymmetric_same_relation:
   (U:Type) (R, R':(Relation U)) (same_relation U R R') ->
            (Antisymmetric U R) -> (Antisymmetric U R').
-Intuition.
+Proof.
+  Compute;Intros;Elim H;Intros;Clear H;Apply (H0 x y (H3 x y H1) (H3 y x H2)).
+(*Intuition.*)
 Qed.
 
 Theorem cong_transitive_same_relation: