diff options
| author |  msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-10-05 22:43:56 +0000 |
|---|---|---|
| committer | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-10-05 22:43:56 +0000 |
| commit | dd7a12f1a2caddef510ad857f0183ae3501b05ac (patch) | |
| tree | 5346794991eea35ae0b0e34840b5c7b4d8f13604 /theories/Classes | |
| parent | 02a8749f2be324b2fe85897af17d9943dfcd08d7 (diff) | |
Correctly do backtracking during type class resolution even if only new
existentials are generated (at last!). The code simply keeps failure
continuations and apply them if needed.
Fix bottomup and topdown rewrite strategies that looped.
Use auto introduction flag for typeclass instances as well.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12374 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Classes')
| -rw-r--r-- | theories/Classes/RelationClasses.v | 8 |
1 files changed, 5 insertions, 3 deletions
diff --git a/theories/Classes/RelationClasses.v b/theories/Classes/RelationClasses.v index 0222ad115..bc25fe488 100644 --- a/theories/Classes/RelationClasses.v +++ b/theories/Classes/RelationClasses.v @@ -358,12 +358,14 @@ Definition relation_disjunction {A} (R : relation A) (R' : relation A) : relatio (** Relation equivalence is an equivalence, and subrelation defines a partial order. *) +Set Automatic Introduction. + Instance relation_equivalence_equivalence (A : Type) : Equivalence (@relation_equivalence A). -Proof. intro A. exact (@predicate_equivalence_equivalence (cons A (cons A nil))). Qed. +Proof. exact (@predicate_equivalence_equivalence (cons A (cons A nil))). Qed. -Instance relation_implication_preorder : PreOrder (@subrelation A). -Proof. intro A. exact (@predicate_implication_preorder (cons A (cons A nil))). Qed. +Instance relation_implication_preorder A : PreOrder (@subrelation A). +Proof. exact (@predicate_implication_preorder (cons A (cons A nil))). Qed. (** *** Partial Order. A partial order is a preorder which is additionally antisymmetric. |