diff options
| author |  msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-01-11 16:59:34 +0000 |
|---|---|---|
| committer | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-01-11 16:59:34 +0000 |
| commit | 1b39b6f1cea94464dbbfb683ad69de18482d4846 (patch) | |
| tree | baf8ce67dfa3df4acde7710012448291f2dcac24 /theories/Classes/RelationClasses.v | |
| parent | 661e782b0334cd448fd372a92bc8901b1654189a (diff) | |
Add [Typeclasses Debug] option that respects backtracking, solve
regression in typeclass resolution not generating the proper subgoals
(may break some contribs).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13787 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Classes/RelationClasses.v')
| -rw-r--r-- | theories/Classes/RelationClasses.v | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/theories/Classes/RelationClasses.v b/theories/Classes/RelationClasses.v index 7116383c8..13342aefd 100644 --- a/theories/Classes/RelationClasses.v +++ b/theories/Classes/RelationClasses.v @@ -141,9 +141,9 @@ Program Instance impl_Transitive : Transitive impl. (** Logical equivalence. *) -Program Instance iff_Reflexive : Reflexive iff. -Program Instance iff_Symmetric : Symmetric iff. -Program Instance iff_Transitive : Transitive iff. +Instance iff_Reflexive : Reflexive iff := iff_refl. +Instance iff_Symmetric : Symmetric iff := iff_sym. +Instance iff_Transitive : Transitive iff := iff_trans. (** Leibniz equality. *) @@ -313,6 +313,7 @@ Notation "∙⊥∙" := false_predicate : predicate_scope. (** Predicate equivalence is an equivalence, and predicate implication defines a preorder. *) Program Instance predicate_equivalence_equivalence : Equivalence (@predicate_equivalence l). + Next Obligation. induction l ; firstorder. Qed. |