- 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

2 files changed, 3 insertions, 2 deletions

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: