Debug implementation of failing tactics in Morphism to allow earlier

failures in proof search. Catch Refiner.FailError in typeclasses eauto
to indicate that an extern tactic failed.


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

3 files changed, 43 insertions, 10 deletions

diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4
index d6de5e69d..4319a1d3d 100644
--- a/tactics/class_tactics.ml4
+++ b/tactics/class_tactics.ml4
@@ -161,6 +161,11 @@ let filter_hyp t =
     | Evar _ | Meta _ | Sort _ -> false
     | _ -> true
 
+let rec catchable = function
+  | Refiner.FailError _ -> true
+  | Stdpp.Exc_located (_, e) -> catchable e
+  | e -> Logic.catchable_exception e
+
 module SearchProblem = struct
     
   type state = search_state
@@ -194,9 +199,7 @@ module SearchProblem = struct
 (* 	      		    msg (hov 1 (pptac ++ str" gives: \n" ++ pr_goals lgls ++ str"\n")) *)
 (* 	      		end; *)
 	      ((lgls,v'),pri,pptac) :: aux tacl
-	  with e when Logic.catchable_exception e ->
-	    (* 	    if !debug then msg (str"failed\n"); *)
-	    aux tacl
+	  with e when catchable e -> aux tacl
     in aux l
       
   let nb_empty_evars s = 
diff --git a/theories/Classes/Morphisms.v b/theories/Classes/Morphisms.v
index be0ea7810..5ac6d8ee5 100644
--- a/theories/Classes/Morphisms.v
+++ b/theories/Classes/Morphisms.v
@@ -114,7 +114,7 @@ Inductive subrelation_done : Prop :=
 
 Ltac subrelation_tac := 
   match goal with
-    | [ _ : subrelation_done |- _ ] => fail
+    | [ _ : subrelation_done |- _ ] => fail 1
     | [ |- @Morphism _ _ _ ] => let H := fresh "H" in
       set(H:=did_subrelation) ; eapply @subrelation_morphism
   end.
@@ -336,8 +336,38 @@ Proof. firstorder. Qed.
 
 (** [R] is Reflexive, hence we can build the needed proof. *)
 
-Program Instance [ Morphism (A -> B) (R ==> R') m, Reflexive A R ]  =>
-  Reflexive_partial_app_morphism : Morphism R' (m x) | 4.
+Lemma Reflexive_partial_app_morphism [ Morphism (A -> B) (R ==> R') m, Reflexive A R ] (x : A) :
+   Morphism R' (m x).
+Proof. simpl_relation. Qed.
+
+Ltac partial_application_tactic := 
+  let tac x :=
+    match type of x with
+      | Type => fail 1
+      | _ => eapply @Reflexive_partial_app_morphism
+    end
+  in
+  let on_morphism m :=
+    match m with
+      | ?m' ?x => tac x
+      | ?m' _ ?x => tac x
+      | ?m' _ _ ?x => tac x
+      | ?m' _ _ _ ?x => tac x
+      | ?m' _ _ _ _ ?x => tac x
+      | ?m' _ _ _ _ _ ?x => tac x
+      | ?m' _ _ _ _ _ _ ?x => tac x
+      | ?m' _ _ _ _ _ _ _ ?x => tac x
+      | ?m' _ _ _ _ _ _ _ _ ?x => tac x
+    end
+  in
+  match goal with
+    | [ |- @Morphism _ _ ?m ] => on_morphism m
+  end.
+
+(* Program Instance [ Morphism (A -> B) (R ==> R') m, Reflexive A R ] (x : A) => *)
+(*   reflexive_partial_app_morphism : Morphism R' (m x). *)
+
+Hint Extern 4 (@Morphism _ _ _) => partial_application_tactic : typeclass_instances.
 
 Lemma inverse_respectful : forall (A : Type) (R : relation A) (B : Type) (R' : relation B),
   relation_equivalence (inverse (R ==> R')) (inverse R ==> inverse R').
@@ -402,7 +432,7 @@ Inductive normalization_done : Prop := did_normalization.
 
 Ltac morphism_normalization := 
   match goal with
-    | [ _ : normalization_done |- _ ] => fail
+    | [ _ : normalization_done |- _ ] => fail 1
     | [ |- @Morphism _ _ _ ] => let H := fresh "H" in
       set(H:=did_normalization) ; eapply @morphism_releq_morphism
   end.
@@ -417,8 +447,8 @@ Proof. firstorder. Qed.
 
 Ltac morphism_reflexive :=
   match goal with
-    | [ _ : normalization_done |- _ ] => fail
-    | [ _ : subrelation_done |- _ ] => fail
+    | [ _ : normalization_done |- _ ] => fail 1
+    | [ _ : subrelation_done |- _ ] => fail 1
     | [ |- @Morphism _ _ _ ] => eapply @reflexive_morphism
   end.
 
diff --git a/theories/Classes/SetoidClass.v b/theories/Classes/SetoidClass.v
index 3220f599c..d22398166 100644
--- a/theories/Classes/SetoidClass.v
+++ b/theories/Classes/SetoidClass.v
@@ -131,7 +131,7 @@ Implicit Arguments setoid_morphism [[!sa]].
 Existing Instance setoid_morphism.
 
 Program Definition setoid_partial_app_morphism [ sa : Setoid A ] (x : A) : Morphism (equiv ++> iff) (equiv x) :=
-  Reflexive_partial_app_morphism.
+  Reflexive_partial_app_morphism x.
 
 Existing Instance setoid_partial_app_morphism.