diff options
| author |  filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-02-01 08:35:21 +0000 |
|---|---|---|
| committer | filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-02-01 08:35:21 +0000 |
| commit | c300bc395fb987f7ded64c17bce5c966c0279442 (patch) | |
| tree | 443364b05d14feb412ba7a1a66ebc6ee1b6d8b2e /theories/Sets/Relations_1_facts.v | |
| parent | 1fda9cc1a2d8c2db92d88d3e2715d3ee86f90bf3 (diff) | |
- 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
Diffstat (limited to 'theories/Sets/Relations_1_facts.v')
| -rwxr-xr-x | theories/Sets/Relations_1_facts.v | 2 |
1 files changed, 1 insertions, 1 deletions
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: |