diff options
| -rw-r--r-- | tactics/class_tactics.ml4 | 19 | ||||
| -rw-r--r-- | theories/Classes/Morphisms.v | 15 |
2 files changed, 29 insertions, 5 deletions
diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4 index 90be325a6e..60bdc8e031 100644 --- a/tactics/class_tactics.ml4 +++ b/tactics/class_tactics.ml4 @@ -616,6 +616,12 @@ let unify_eqn gl hypinfo t = in Some (env', res) with _ -> None +let unfold_impl t = + match kind_of_term t with + | App (arrow, [| a; b |]) when eq_constr arrow (Lazy.force impl) -> + mkProd (Anonymous, a, b) + | _ -> t + let build_new gl env sigma occs hypinfo concl cstr evars = let is_occ occ = occs = [] || List.mem occ occs in let rec aux t occ cstr = @@ -658,9 +664,14 @@ let build_new gl env sigma occs hypinfo concl cstr evars = let res = if x' = None && b' = None then None else - (try Some (resolve_morphism env sigma t - (arrow_morphism (pf_type_of gl x) (pf_type_of gl b)) [| x ; b |] [| x' ; b' |] - cstr evars) + (try + let (proof, (a, r, oldt, newt)) = + resolve_morphism env sigma t + (arrow_morphism (pf_type_of gl x) (pf_type_of gl b)) [| x ; b |] [| x' ; b' |] + cstr evars + in + let newt' = unfold_impl newt in + Some (proof, (a, r, oldt, newt')) with Not_found -> None) in res, occ @@ -755,7 +766,7 @@ let cl_rewrite_clause_aux hypinfo goal_meta occs clause gl = let evd = Evd.evars_of undef in if not (evd = Evd.empty) then Refiner.tclEVARS (Evd.merge sigma evd) else tclIDTAC - in tclTHENLIST [evartac; rewtac; cleantac] gl + in tclTHENLIST [evartac; rewtac(* ; cleantac *)] gl with UserError (env, e) -> tclFAIL 0 (str" setoid rewrite failed: unable to satisfy the rewriting constraints") gl) | None -> diff --git a/theories/Classes/Morphisms.v b/theories/Classes/Morphisms.v index 1ba1f585ae..0087916c30 100644 --- a/theories/Classes/Morphisms.v +++ b/theories/Classes/Morphisms.v @@ -241,8 +241,21 @@ Program Instance {A B C : Type} [ Morphism (RA ==> RB ==> RC) (f : A -> B -> C) (* apply respect. *) (* Qed. *) +(** Every morphism gives rise to a morphism on the inverse relation. *) -(** Morpshism declarations for partial applications. *) +Program Instance (A : Type) (R : relation A) (B : Type) (R' : relation B) + [ Morphism (R ==> R') m ] => morphism_inverse_morphism : + Morphism (inverse R ==> inverse R') m. + + Next Obligation. + Proof. + unfold inverse in *. + pose respect. + unfold respectful in r. + apply r ; auto. + Qed. + +(** Morphism declarations for partial applications. *) Program Instance [ ! Transitive A R ] (x : A) => trans_contra_inv_impl_morphism : Morphism (R --> inverse impl) (R x). |