Add a missing morphism declaration that turns morphisms on R ==> R' to

morphisms on R --> inverse R' for any R, R' (report by N. Tabareau). 
Better implementation of unfolding for impl that does it only where
necessary to keep the goal in the same shape as the user gave.


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

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).