From c300bc395fb987f7ded64c17bce5c966c0279442 Mon Sep 17 00:00:00 2001 From: filliatr Date: Thu, 1 Feb 2001 08:35:21 +0000 Subject: - 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) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1304 85f007b7-540e-0410-9357-904b9bb8a0f7 --- theories/Sets/Partial_Order.v | 3 ++- theories/Sets/Relations_1_facts.v | 2 +- 2 files changed, 3 insertions(+), 2 deletions(-) (limited to 'theories/Sets') 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: -- cgit v1.2.3