diff options
| -rw-r--r-- | tactics/class_tactics.ml4 | 9 | ||||
| -rw-r--r-- | theories/Classes/Morphisms.v | 42 | ||||
| -rw-r--r-- | theories/Classes/SetoidClass.v | 2 |
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. |