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

2 files changed, 29 insertions, 25 deletions

diff --git a/theories/Classes/Morphisms.v b/theories/Classes/Morphisms.v
index 04688b00f..55199cdea 100644
--- a/theories/Classes/Morphisms.v
+++ b/theories/Classes/Morphisms.v
@@ -408,41 +408,45 @@ Class PartialApplication.
 CoInductive normalization_done : Prop := did_normalization.
 
 Ltac partial_application_tactic :=
-  let rec do_partial_apps H m :=
+  let rec do_partial_apps H m cont := 
     match m with
-      | ?m' ?x => class_apply @Reflexive_partial_app_morphism ; [do_partial_apps H m'|clear H]
-      | _ => idtac
+      | ?m' ?x => class_apply @Reflexive_partial_app_morphism ; 
+        [(do_partial_apps H m' ltac:idtac)|clear H]
+      | _ => cont
     end
   in
-  let rec do_partial H ar m :=
+  let rec do_partial H ar m := 
     match ar with
-      | 0 => do_partial_apps H m
+      | 0%nat => do_partial_apps H m ltac:(fail 1)
       | S ?n' =>
         match m with
           ?m' ?x => do_partial H n' m'
         end
     end
   in
-  let on_morphism m :=
-    let m' := fresh in head_of_constr m' m ;
-    let n := fresh in evar (n:nat) ;
-    let v := eval compute in n in clear n ;
-    let H := fresh in
-      assert(H:Params m' v) by typeclasses eauto ;
-      let v' := eval compute in v in subst m';
-      do_partial H v' m
- in
+  let params m sk fk :=
+    (let m' := fresh in head_of_constr m' m ;
+     let n := fresh in evar (n:nat) ;
+     let v := eval compute in n in clear n ;
+      let H := fresh in
+        assert(H:Params m' v) by typeclasses eauto ;
+          let v' := eval compute in v in subst m';
+            (sk H v' || fail 1))
+    || fk
+  in
+  let on_morphism m cont :=
+    params m ltac:(fun H n => do_partial H n m)
+      ltac:(cont)
+  in
   match goal with
     | [ _ : normalization_done |- _ ] => fail 1
     | [ _ : @Params _ _ _ |- _ ] => fail 1
     | [ |- @Proper ?T _ (?m ?x) ] =>
       match goal with
-        | [ _ : PartialApplication |- _ ] =>
-          class_apply @Reflexive_partial_app_morphism
-        | _ =>
-          on_morphism (m x) ||
-            (class_apply @Reflexive_partial_app_morphism ;
-              [ pose Build_PartialApplication | idtac ])
+        | [ H : PartialApplication |- _ ] =>
+          class_apply @Reflexive_partial_app_morphism; [|clear H]
+        | _ => on_morphism (m x)
+          ltac:(class_apply @Reflexive_partial_app_morphism)
       end
   end.
 
@@ -471,7 +475,7 @@ Qed.
 
 Lemma inverse_arrow `(NA : Normalizes A R (inverse R'''), NB : Normalizes B R' (inverse R'')) :
   Normalizes (A -> B) (R ==> R') (inverse (R''' ==> R'')%signature).
-Proof. unfold Normalizes in *. intros.
+Proof. unfold Normalizes in *. intros. 
   rewrite NA, NB. firstorder.
 Qed.
 
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. *)