Merge subinstances branch by me and Tom Prince.

This adds two experimental features to the typeclass implementation:
- Path cuts: a way to specify through regular expressions on instance names
search pathes that should be avoided (e.g. [proper_flip proper_flip]).
Regular expression matching is implemented through naïve derivatives.
- Forward hints for subclasses: e.g. [Equivalence -> Reflexive] is no
longer applied backwards, but introducing a specific [Equivalence] in the
environment register a [Reflexive] hint as well. Currently not
backwards-compatible, the next patch will allow to specify direction
of subclasses hints.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14671 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 4 insertions, 4 deletions

diff --git a/theories/Classes/RelationClasses.v b/theories/Classes/RelationClasses.v
index 397328a11..3a34e3a11 100644
--- a/theories/Classes/RelationClasses.v
+++ b/theories/Classes/RelationClasses.v
@@ -156,14 +156,14 @@ Instance eq_Transitive {A} : Transitive (@eq A) := @eq_trans A.
 (** A [PreOrder] is both Reflexive and Transitive. *)
 
 Class PreOrder {A} (R : relation A) : Prop := {
-  PreOrder_Reflexive :> Reflexive R ;
-  PreOrder_Transitive :> Transitive R }.
+  PreOrder_Reflexive :> Reflexive R | 2 ;
+  PreOrder_Transitive :> Transitive R | 2 }.
 
 (** A partial equivalence relation is Symmetric and Transitive. *)
 
 Class PER {A} (R : relation A) : Prop := {
-  PER_Symmetric :> Symmetric R ;
-  PER_Transitive :> Transitive R }.
+  PER_Symmetric :> Symmetric R | 3 ;
+  PER_Transitive :> Transitive R | 3 }.
 
 (** Equivalence relations. *)