Plug the new setoid implemtation in, leaving the original one commented

out. The semantics of the old setoid are faithfully simulated by the new
tactic, hence no scripts involving rewrite are modified. However,
parametric morphism declarations need to be changed, but there are only a
few in the standard library, notably in FSets. The declaration and the
introduction of variables in the script need to be tweaked a bit,
otherwise the proofs remain unchanged. 
Some fragile scripts not introducting their variable names explicitely
were broken. Requiring Setoid requires Program.Basics which sets stronger
implicit arguments on some constants, a few scripts benefit from that.
Ring/field have been ported but do not really use the new typeclass
architecture as well as they could. Performance should be mostly
unchanged, but will certainly improve in the near future. Size of the
vo's seems not to have changed at all.
It will certainly break some contribs using Setoid.


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

28 files changed, 925 insertions, 335 deletions

diff --git a/Makefile.common b/Makefile.common
index 73c76e5a43..d4dc8256f0 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -743,7 +743,7 @@ INTEGERVO:=$(INTEGERABSTRACTVO) $(INTEGERBINARYVO) $(INTEGERNATPAIRSVO) $(INTEGE
 
 NUMBERSVO:= $(NUMBERSCOMMONVO) $(NATURALVO) $(INTEGERVO) $(NATINTVO)
 
-SETOIDSVO:= theories/Setoids/Setoid_tac.vo theories/Setoids/Setoid_Prop.vo theories/Setoids/Setoid.vo
+SETOIDSVO:= theories/Setoids/Setoid.vo # theories/Setoids/Setoid_tac.vo theories/Setoids/Setoid_Prop.vo
 
 UNICODEVO:= theories/Unicode/Utf8.vo
 
diff --git a/contrib/ring/Setoid_ring_theory.v b/contrib/ring/Setoid_ring_theory.v
index 4ec8433fe5..f50a2f30a4 100644
--- a/contrib/ring/Setoid_ring_theory.v
+++ b/contrib/ring/Setoid_ring_theory.v
@@ -245,7 +245,7 @@ Lemma Saux1 : forall a:A, a + a == a -> a == 0.
 intros.
 rewrite <- (plus_zero_left a).
 rewrite (plus_comm 0 a).
-setoid_replace (a + 0) with (a + (a + - a)); auto.
+setoid_replace (a + 0) with (a + (a + - a)) by auto.
 rewrite (plus_assoc a a (- a)).
 rewrite H.
 apply opp_def.
diff --git a/contrib/rtauto/Bintree.v b/contrib/rtauto/Bintree.v
index 67a952b73f..d410606a74 100644
--- a/contrib/rtauto/Bintree.v
+++ b/contrib/rtauto/Bintree.v
@@ -107,7 +107,7 @@ intro ne;right;congruence.
 left;reflexivity.
 Defined.
 
-Theorem pos_eq_dec_refl : forall m, pos_eq_dec m m = left (m<>m) (refl_equal m) .
+Theorem pos_eq_dec_refl : forall m, pos_eq_dec m m = left (refl_equal m).
 fix 1;intros [mm|mm|].
 simpl; rewrite  pos_eq_dec_refl; reflexivity.
 simpl; rewrite  pos_eq_dec_refl; reflexivity.
@@ -116,7 +116,7 @@ Qed.
 
 Theorem pos_eq_dec_ex : forall m n,
  pos_eq m n =true -> exists h:m=n,
- pos_eq_dec m n = left (m<>n) h.
+ pos_eq_dec m n = left h.
 fix 1;intros [mm|mm|] [nn|nn|];try (simpl;congruence).
 simpl;intro e.
 elim (pos_eq_dec_ex _ _ e).
diff --git a/contrib/setoid_ring/InitialRing.v b/contrib/setoid_ring/InitialRing.v
index 6542d280c8..56b08a8fa1 100644
--- a/contrib/setoid_ring/InitialRing.v
+++ b/contrib/setoid_ring/InitialRing.v
@@ -243,7 +243,7 @@ Section ZMORPHISM.
                   Zplus Zmult Zeq_bool gen_phiZ).
    apply mkRmorph;simpl;try rrefl.
    apply gen_phiZ_add.  apply gen_phiZ_mul. apply gen_Zeqb_ok.
-  apply  (Smorph_morph Rsth Reqe Rth Zsth Zth SRmorph gen_phiZ_ext).
+  apply  (Smorph_morph Rsth Reqe Rth Zth SRmorph gen_phiZ_ext).
  Qed.
 
 End ZMORPHISM.
diff --git a/contrib/setoid_ring/Ring_theory.v b/contrib/setoid_ring/Ring_theory.v
index caa704595c..cefdcf52b8 100644
--- a/contrib/setoid_ring/Ring_theory.v
+++ b/contrib/setoid_ring/Ring_theory.v
@@ -59,8 +59,7 @@ Section Power.
   induction j;simpl.
   rewrite IHj.
   rewrite (mul_comm x (pow_pos x j *pow_pos x j)).
-  set (w:= x*pow_pos x j);unfold w at 2.
-  rewrite (mul_comm x (pow_pos x j));unfold w.
+  setoid_rewrite (mul_comm x (pow_pos x j)) at 2.
   repeat rewrite mul_assoc. apply (Seq_refl _ _ Rsth).
   repeat rewrite mul_assoc. apply (Seq_refl _ _ Rsth).
   apply (Seq_refl _ _ Rsth).
diff --git a/contrib/setoid_ring/newring.ml4 b/contrib/setoid_ring/newring.ml4
index 6c3b6337af..bce41b9b5f 100644
--- a/contrib/setoid_ring/newring.ml4
+++ b/contrib/setoid_ring/newring.ml4
@@ -201,7 +201,8 @@ let constr_of = function
 let stdlib_modules =
   [["Coq";"Setoids";"Setoid"];
    ["Coq";"Lists";"List"];
-   ["Coq";"Init";"Datatypes"]
+   ["Coq";"Init";"Datatypes"];
+   ["Coq";"Init";"Logic"];
   ]
 
 let coq_constant c =
@@ -212,6 +213,7 @@ let coq_cons = coq_constant "cons"
 let coq_nil = coq_constant "nil"
 let coq_None = coq_constant "None"
 let coq_Some = coq_constant "Some"
+let coq_eq = coq_constant "eq"
 
 let lapp f args = mkApp(Lazy.force f,args)
 
@@ -448,10 +450,12 @@ let (theory_to_obj, obj_to_theory) =
       export_function = export_th }
 
 
-let setoid_of_relation r =
+let setoid_of_relation env a r =
   lapp coq_mk_Setoid
-    [|r.rel_a; r.rel_aeq;
-      Option.get r.rel_refl; Option.get r.rel_sym; Option.get r.rel_trans |]
+    [|a ; r ; 
+      Class_tactics.reflexive_proof env a r ; 
+      Class_tactics.symmetric_proof env a r ; 
+      Class_tactics.transitive_proof env a r |]
 
 let op_morph r add mul opp req m1 m2 m3 =
   lapp coq_mk_reqe [| r; add; mul; opp; req; m1; m2; m3 |]
@@ -459,63 +463,108 @@ let op_morph r add mul opp req m1 m2 m3 =
 let op_smorph r add mul req m1 m2 =
   lapp coq_mk_seqe [| r; add; mul; req; m1; m2 |]
 
-let default_ring_equality (r,add,mul,opp,req) =
-  let is_setoid = function
-      {rel_refl=Some _; rel_sym=Some _;rel_trans=Some _;rel_aeq=rel} ->
-        eq_constr req rel (* Qu: use conversion ? *)
-    | _ -> false in
-  match default_relation_for_carrier ~filter:is_setoid r with
-      Leibniz _ ->
-        let setoid = lapp coq_eq_setoid [|r|] in
-        let op_morph =
-          match opp with
+(* let default_ring_equality (r,add,mul,opp,req) = *)
+(*   let is_setoid = function *)
+(*       {rel_refl=Some _; rel_sym=Some _;rel_trans=Some _;rel_aeq=rel} -> *)
+(*         eq_constr req rel (\* Qu: use conversion ? *\) *)
+(*     | _ -> false in *)
+(*   match default_relation_for_carrier ~filter:is_setoid r with *)
+(*       Leibniz _ -> *)
+(*         let setoid = lapp coq_eq_setoid [|r|] in *)
+(*         let op_morph = *)
+(*           match opp with *)
+(*               Some opp -> lapp coq_eq_morph [|r;add;mul;opp|] *)
+(*             | None -> lapp coq_eq_smorph [|r;add;mul|] in *)
+(*         (setoid,op_morph) *)
+(*     | Relation rel -> *)
+(*         let setoid = setoid_of_relation rel in *)
+(*         let is_endomorphism = function *)
+(*             { args=args } -> List.for_all *)
+(*                 (function (var,Relation rel) -> *)
+(*                   var=None && eq_constr req rel *)
+(*                   | _ -> false) args in *)
+(*         let add_m = *)
+(*           try default_morphism ~filter:is_endomorphism add *)
+(*           with Not_found -> *)
+(*             error "ring addition should be declared as a morphism" in *)
+(*         let mul_m = *)
+(*           try default_morphism ~filter:is_endomorphism mul *)
+(*           with Not_found -> *)
+(*             error "ring multiplication should be declared as a morphism" in *)
+(*         let op_morph = *)
+(*           match opp with *)
+(*             | Some opp -> *)
+(*             (let opp_m = *)
+(*               try default_morphism ~filter:is_endomorphism opp *)
+(*               with Not_found -> *)
+(*                 error "ring opposite should be declared as a morphism" in *)
+(*              let op_morph = *)
+(*                op_morph r add mul opp req add_m.lem mul_m.lem opp_m.lem in *)
+(*              msgnl *)
+(*                (str"Using setoid \""++pr_constr rel.rel_aeq++str"\""++spc()++   *)
+(*                str"and morphisms \""++pr_constr add_m.morphism_theory++ *)
+(*                str"\","++spc()++ str"\""++pr_constr mul_m.morphism_theory++ *)
+(*                str"\""++spc()++str"and \""++pr_constr opp_m.morphism_theory++ *)
+(*                str"\""); *)
+(*              op_morph) *)
+(*             | None -> *)
+(*             (msgnl *)
+(*               (str"Using setoid \""++pr_constr rel.rel_aeq++str"\"" ++ spc() ++   *)
+(*                str"and morphisms \""++pr_constr add_m.morphism_theory++ *)
+(*                str"\""++spc()++str"and \""++ *)
+(*                pr_constr mul_m.morphism_theory++str"\""); *)
+(*             op_smorph r add mul req add_m.lem mul_m.lem) in *)
+(*         (setoid,op_morph) *)
+
+let ring_equality (r,add,mul,opp,req) =
+  match kind_of_term req with
+    | App (f, [| _ |]) when eq_constr f (Lazy.force coq_eq) ->
+	let setoid = lapp coq_eq_setoid [|r|] in
+	let op_morph =
+	  match opp with
               Some opp -> lapp coq_eq_morph [|r;add;mul;opp|]
             | None -> lapp coq_eq_smorph [|r;add;mul|] in
-        (setoid,op_morph)
-    | Relation rel ->
-        let setoid = setoid_of_relation rel in
-        let is_endomorphism = function
-            { args=args } -> List.for_all
-                (function (var,Relation rel) ->
-                  var=None && eq_constr req rel
-                  | _ -> false) args in
-        let add_m =
-          try default_morphism ~filter:is_endomorphism add
+	  (setoid,op_morph)
+    | _ ->
+	let setoid = setoid_of_relation (Global.env ()) r req in
+	let signature = [Some (r,req);Some (r,req);Some(r,req)] in
+	let add_m, add_m_lem =
+	  try Class_tactics.default_morphism signature add
           with Not_found ->
             error "ring addition should be declared as a morphism" in
-        let mul_m =
-          try default_morphism ~filter:is_endomorphism mul
+	let mul_m, mul_m_lem =
+          try Class_tactics.default_morphism signature mul
           with Not_found ->
             error "ring multiplication should be declared as a morphism" in
         let op_morph =
           match opp with
             | Some opp ->
-            (let opp_m =
-              try default_morphism ~filter:is_endomorphism opp
-              with Not_found ->
-                error "ring opposite should be declared as a morphism" in
-             let op_morph =
-               op_morph r add mul opp req add_m.lem mul_m.lem opp_m.lem in
-             msgnl
-               (str"Using setoid \""++pr_constr rel.rel_aeq++str"\""++spc()++  
-               str"and morphisms \""++pr_constr add_m.morphism_theory++
-               str"\","++spc()++ str"\""++pr_constr mul_m.morphism_theory++
-               str"\""++spc()++str"and \""++pr_constr opp_m.morphism_theory++
-               str"\"");
-             op_morph)
+		(let opp_m,opp_m_lem =
+		  try Class_tactics.default_morphism (List.tl signature) opp
+		  with Not_found ->
+                    error "ring opposite should be declared as a morphism" in
+		let op_morph =
+		  op_morph r add mul opp req add_m_lem mul_m_lem opp_m_lem in
+		  msgnl
+		    (str"Using setoid \""++pr_constr req++str"\""++spc()++  
+			str"and morphisms \""++pr_constr add_m ++
+			str"\","++spc()++ str"\""++pr_constr mul_m++
+			str"\""++spc()++str"and \""++pr_constr opp_m++
+			str"\"");
+		  op_morph)
             | None ->
-            (msgnl
-              (str"Using setoid \""++pr_constr rel.rel_aeq++str"\"" ++ spc() ++  
-               str"and morphisms \""++pr_constr add_m.morphism_theory++
-               str"\""++spc()++str"and \""++
-               pr_constr mul_m.morphism_theory++str"\"");
-            op_smorph r add mul req add_m.lem mul_m.lem) in
-        (setoid,op_morph)
-
+		(msgnl
+		    (str"Using setoid \""++pr_constr req ++str"\"" ++ spc() ++  
+			str"and morphisms \""++pr_constr add_m ++
+			str"\""++spc()++str"and \""++
+			pr_constr mul_m++str"\"");
+		 op_smorph r add mul req add_m_lem mul_m_lem) in
+          (setoid,op_morph)
+	    
 let build_setoid_params r add mul opp req eqth =
   match eqth with
       Some th -> th
-    | None -> default_ring_equality (r,add,mul,opp,req)
+    | None -> ring_equality (r,add,mul,opp,req)
 
 let dest_ring env sigma th_spec =
   let th_typ = Retyping.get_type_of env sigma th_spec in
@@ -980,25 +1029,19 @@ let (ftheory_to_obj, obj_to_ftheory) =
       classify_function = (fun (_,x) -> Substitute x);
       export_function = export_th }
 
-let default_field_equality r inv req =
-  let is_setoid = function
-      {rel_refl=Some _; rel_sym=Some _;rel_trans=Some _} -> true
-    | _ -> false in
-  match default_relation_for_carrier ~filter:is_setoid r with
-      Leibniz _ ->
+let field_equality r inv req =
+  match kind_of_term req with
+    | App (f, [| _ |]) when eq_constr f (Lazy.force coq_eq) ->
         mkApp((Coqlib.build_coq_eq_data()).congr,[|r;r;inv|])
-    | Relation rel ->
-        let is_endomorphism = function
-            { args=args } -> List.for_all
-                (function (var,Relation rel) ->
-                  var=None && eq_constr req rel
-                  | _ -> false) args in
-        let inv_m =
-          try default_morphism ~filter:is_endomorphism inv
+    | _ ->
+	let _setoid = setoid_of_relation (Global.env ()) r req in
+	let signature = [Some (r,req);Some(r,req)] in
+	let inv_m, inv_m_lem =
+	  try Class_tactics.default_morphism signature inv
           with Not_found ->
             error "field inverse should be declared as a morphism" in
-        inv_m.lem
-
+	  inv_m_lem
+	    
 let add_field_theory name fth eqth morphth cst_tac inj (pre,post) power sign odiv =
   check_required_library (cdir@["Field_tac"]);
   let env = Global.env() in
@@ -1011,7 +1054,7 @@ let add_field_theory name fth eqth morphth cst_tac inj (pre,post) power sign odi
   let (pow_tac, pspec) = interp_power env power in 
   let sspec = interp_sign env sign in
   let dspec = interp_div env odiv in
-  let inv_m = default_field_equality r inv req in
+  let inv_m = field_equality r inv req in
   let rk = reflect_coeff morphth in
   let params =
     exec_tactic env 9 (field_ltac"field_lemmas")
diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4
index 86a1081ec3..c27e6b05de 100644
--- a/tactics/class_tactics.ml4
+++ b/tactics/class_tactics.ml4
@@ -32,6 +32,10 @@ open Rawterm
 open Hiddentac
 open Typeclasses
 open Typeclasses_errors
+open Classes
+open Topconstr
+open Pfedit
+open Command
 
 open Evd
 
@@ -69,9 +73,9 @@ let rec e_trivial_fail_db db_list local_db goal =
 and e_my_find_search db_list local_db hdc concl = 
   let hdc = head_of_constr_reference hdc in
   let hintl =
-    if occur_existential concl then 
+    if occur_existential concl then
       list_map_append (Hint_db.map_all hdc) (local_db::db_list)
-    else 
+    else
       list_map_append (Hint_db.map_auto (hdc,concl)) (local_db::db_list)
   in 
   let tac_of_hint = 
@@ -101,9 +105,9 @@ and e_trivial_resolve db_list local_db gl =
   with Bound | Not_found -> []
 
 let e_possible_resolve db_list local_db gl =
-  try List.map snd
-    (e_my_find_search db_list local_db 
-	(List.hd (head_constr_bound gl [])) gl)
+  try 
+    List.map snd (e_my_find_search db_list local_db 
+		       (List.hd (head_constr_bound gl [])) gl)
   with Bound | Not_found -> []
 
 let find_first_goal gls = 
@@ -121,6 +125,8 @@ module SearchProblem = struct
     
   type state = search_state
 
+  let debug = ref false
+
   let success s = (sig_it (fst s.tacres)) = []
 
   let pr_ev evs ev = Printer.pr_constr_env (Evd.evar_env ev) (Evarutil.nf_evar evs ev.Evd.evar_concl)
@@ -139,19 +145,29 @@ module SearchProblem = struct
 	  try 
 	    let (lgls,ptl) = apply_tac_list tac glls in 
 	    let v' p = v (ptl p) in
-(* 	    let gl = Proof_trees.db_pr_goal (List.hd (sig_it glls)) in *)
-(* 	      msg (hov 1 (pptac ++ str" gives: \n" ++ pr_goals lgls ++ str"\n")); *)
+(*               if !debug then *)
+(* 		begin *)
+(* 		  let evars = Evarutil.nf_evars (Refiner.project glls) in *)
+(* 	            msg (str"Goal:" ++ pr_ev evars (List.hd (sig_it glls)) ++ str"\n"); *)
+(* 		    msg (hov 1 (pptac ++ str" gives: \n" ++ pr_goals lgls ++ str"\n")) *)
+(* 		end; *)
 	      ((lgls,v'),pptac) :: aux tacl
 	  with e when Logic.catchable_exception e ->
 	    aux tacl
     in aux l
 
+  let nb_empty_evars s = 
+    Evd.fold (fun ev evi acc -> if evi.evar_body = Evar_empty then succ acc else acc) s 0
+
   (* Ordering of states is lexicographic on depth (greatest first) then
      number of remaining goals. *)
   let compare s s' =
     let d = s'.depth - s.depth in
-    let nbgoals s = List.length (sig_it (fst s.tacres)) in
-    if d <> 0 then d else nbgoals s - nbgoals s'
+    let nbgoals s = 
+      List.length (sig_it (fst s.tacres)) + 
+	nb_empty_evars (sig_sig (fst s.tacres))
+    in
+      if d <> 0 then d else nbgoals s - nbgoals s'
 
   let branching s = 
     if s.depth = 0 then 
@@ -223,7 +239,8 @@ let make_initial_state n gls dblist localdbs =
 
 let e_depth_search debug p db_list local_dbs gls =
   try
-    let tac = if debug then Search.debug_depth_first else Search.depth_first in
+    let tac = if debug then
+      (SearchProblem.debug := true; Search.debug_depth_first) else Search.depth_first in
     let s = tac (make_initial_state p gls db_list local_dbs) in
     s.tacres
   with Not_found -> error "EAuto: depth first search failed"
@@ -350,6 +367,8 @@ let inverse = lazy (gen_constant ["Classes"; "Relations"] "inverse")
 let respectful_dep = lazy (gen_constant ["Classes"; "Morphisms"] "respectful_dep")
 let respectful = lazy (gen_constant ["Classes"; "Morphisms"] "respectful")
 
+let equivalence = lazy (gen_constant ["Classes"; "Relations"] "Equivalence")
+
 let iff_equiv = lazy (gen_constant ["Classes"; "Relations"] "iff_equivalence")
 let eq_equiv = lazy (gen_constant ["Classes"; "SetoidClass"] "eq_equivalence")
 
@@ -378,7 +397,7 @@ let arrow_morphism a b =
 let setoid_refl pars x = 
   applistc (Lazy.force setoid_refl_proj) (pars @ [x])
       
-let morphism_class = lazy (Lazy.force morphism_class, Lazy.force respect_proj)
+let morphism_class_proj = lazy (Lazy.force morphism_class, Lazy.force respect_proj)
 
 exception Found of (constr * constr * (types * types) list * constr * constr array *
 		       (constr * (constr * constr * constr * constr)) option array)
@@ -390,16 +409,17 @@ let split_head = function
     hd :: tl -> hd, tl
   | [] -> assert(false)
 
-let build_signature isevars env m cstrs finalcstr =
+let build_signature isevars env m (cstrs : 'a option list) (f : 'a -> constr) =
   let new_evar isevars env t =
     Evarutil.e_new_evar isevars env
       (* ~src:(dummy_loc, ImplicitArg (ConstRef (Lazy.force respectful), (n, Some na))) *) t
   in
   let mk_relty ty obj =
-    let relty = coq_relation ty in
-      match obj with
-	| None -> new_evar isevars env relty
-	| Some (p, (a, r, oldt, newt)) -> r
+    match obj with
+      | None -> 
+	  let relty = coq_relation ty in
+	    new_evar isevars env relty
+      | Some x -> f x
   in
   let rec aux t l =
     let t = Reductionops.whd_betadelta env (Evd.evars_of !isevars) t in
@@ -409,36 +429,41 @@ let build_signature isevars env m cstrs finalcstr =
 	  let relty = mk_relty ty obj in
 	  let arg' = mkApp (Lazy.force respectful, [| ty ; relty ; b ; arg |]) in
 	    arg', (ty, relty) :: evars
-      | _, _ -> 
+      | _, [finalcstr] -> 
 	  (match finalcstr with
 	      None -> 
 		let rel = mk_relty t None in 
 		  rel, [t, rel]
 	    | Some (t, rel) -> rel, [t, rel])
+      | _, _ -> assert false
   in aux m cstrs
 
-let reflexivity_proof env evars carrier relation x =
+let reflexivity_proof_evar env evars carrier relation x =
   let goal =
     mkApp (Lazy.force reflexive_type, [| carrier ; relation |])
   in
   let inst = Evarutil.e_new_evar evars env goal in
     (* try resolve_one_typeclass env goal *)
-  mkApp (Lazy.force reflexive_proof, [| carrier ; relation ; inst ; x |])
+    mkApp (Lazy.force reflexive_proof, [| carrier ; relation ; inst ; x |])
     (*     with Not_found -> *)
 (*       let meta = Evarutil.new_meta() in *)
 (* 	mkCast (mkMeta meta, DEFAULTcast, mkApp (relation, [| x; x |])) *)
 
-let symmetric_proof env carrier relation =
+let find_class_proof proof_type proof_method env carrier relation =
   let goal =
-    mkApp (Lazy.force symmetric_type, [| carrier ; relation |])
+    mkApp (Lazy.force proof_type, [| carrier ; relation |])
   in
     try 
       let inst = resolve_one_typeclass env goal in
-	mkApp (Lazy.force symmetric_proof, [| carrier ; relation ; inst |])
+	mkApp (Lazy.force proof_method, [| carrier ; relation ; inst |])
     with e when Logic.catchable_exception e -> raise Not_found
 
+let reflexive_proof env = find_class_proof reflexive_type reflexive_proof env
+let symmetric_proof env = find_class_proof symmetric_type symmetric_proof env
+let transitive_proof env = find_class_proof transitive_type transitive_proof env
+
 let resolve_morphism env sigma oldt m args args' cstr evars =
-  let (morphism_cl, morphism_proj) = Lazy.force morphism_class in
+  let (morphism_cl, morphism_proj) = Lazy.force morphism_class_proj in
   let morph_instance, proj, sigargs, m', args, args' = 
 (*     if is_equiv env sigma m then  *)
 (*       let params, rest = array_chop 3 args in *)
@@ -462,7 +487,8 @@ let resolve_morphism env sigma oldt m args args' cstr evars =
     let morphargs', morphobjs' = array_chop first args' in
     let appm = mkApp(m, morphargs) in
     let appmtype = Typing.type_of env sigma appm in
-    let signature, sigargs = build_signature evars env appmtype (Array.to_list morphobjs') cstr in
+    let cstrs = List.map (function None -> None | Some (_, (a, r, _, _)) -> Some (a, r)) (Array.to_list morphobjs') in
+    let signature, sigargs = build_signature evars env appmtype (cstrs @ [cstr]) (fun (a, r) -> r) in
     let cl_args = [| appmtype ; signature ; appm |] in
     let app = mkApp (mkInd morphism_cl.cl_impl, cl_args) in
     let morph = Evarutil.e_new_evar evars env app in
@@ -478,7 +504,7 @@ let resolve_morphism env sigma oldt m args args' cstr evars =
 	let (carrier, relation), sigargs = split_head sigargs in
 	  match y with
 	      None ->
-		let refl_proof = reflexivity_proof env evars carrier relation x in
+		let refl_proof = reflexivity_proof_evar env evars carrier relation x in
 		  [ refl_proof ; x ; x ] @ acc, sigargs, x :: typeargs'
 	    | Some (p, (_, _, _, t')) ->
 		[ p ; t'; x ] @ acc, sigargs, t' :: typeargs')
@@ -490,93 +516,135 @@ let resolve_morphism env sigma oldt m args args' cstr evars =
 	[ a, r ] -> (proof, (a, r, oldt, newt))
       | _ -> assert(false)
 
-let build_new gl env sigma occs origt newt hyp hypinfo concl cstr evars =
+let rewrite_unif_flags = {
+  Unification.modulo_conv_on_closed_terms = false;
+  Unification.use_metas_eagerly = true;
+  Unification.modulo_conv = false
+}
+
+let rewrite2_unif_flags = {
+  Unification.modulo_conv_on_closed_terms = true;
+  Unification.use_metas_eagerly = true;
+  Unification.modulo_conv = false
+ }
+
+(* let unification_rewrite c1 c2 cl but gl =  *)
+(*   let (env',c1) = *)
+(*     try *)
+(*       (\* ~flags:(false,true) to allow to mark occurences that must not be *)
+(*          rewritten simply by replacing them with let-defined definitions *)
+(*          in the context *\) *)
+(*       w_unify_to_subterm ~flags:rewrite_unif_flags (pf_env gl) (c1,but) cl.evd *)
+(*     with *)
+(* 	Pretype_errors.PretypeError _ -> *)
+(* 	  (\* ~flags:(true,true) to make Ring work (since it really *)
+(*              exploits conversion) *\) *)
+(* 	  w_unify_to_subterm ~flags:rewrite2_unif_flags *)
+(* 	    (pf_env gl) (c1,but) cl.evd *)
+(*   in *)
+(*   let cl' = {cl with evd = env' } in *)
+(*   let c2 = Clenv.clenv_nf_meta cl' c2 in *)
+(*   check_evar_map_of_evars_defs env' ; *)
+(*   env',Clenv.clenv_value cl', c1, c2 *)
+
+let allowK = true
+
+let unify_eqn gl (cl, rel, l2r, c1, c2) t = 
+  try 
+    let env' = 
+      try clenv_unify allowK ~flags:rewrite_unif_flags
+	CONV (if l2r then c1 else c2) t cl
+      with Pretype_errors.PretypeError _ -> (* For Ring essentially *)
+	clenv_unify allowK ~flags:rewrite2_unif_flags
+	  CONV (if l2r then c1 else c2) t cl
+    in
+    let c1 = Clenv.clenv_nf_meta env' c1 
+    and c2 = Clenv.clenv_nf_meta env' c2 
+    and typ = Clenv.clenv_type env' in
+    let (rel, args) = destApp typ in
+    let relargs, args = array_chop (Array.length args - 2) args in
+    let rel = mkApp (rel, relargs) in
+    let car = pf_type_of gl c1 in
+    let prf = Clenv.clenv_value env' in
+    let res = 
+      if l2r then (prf, (car, rel, c1, c2))
+      else
+	try (mkApp (symmetric_proof (pf_env gl) car rel, [| c1 ; c2 ; prf |]), (car, rel, c2, c1))
+	with Not_found ->
+	  (prf, (car, mkApp (Lazy.force inverse, [| car ; rel |]), c2, c1))
+    in Some (env', res)
+  with _ -> None
+
+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 =
-    match kind_of_term t with
-      | _ when eq_constr t origt -> 
-	  if is_occ occ then
+    match unify_eqn gl hypinfo t with
+      | Some (env', (prf, hypinfo as x)) ->
+	  if is_occ occ then (
+	    evars := Evd.evar_merge !evars (Evd.evars_of (Evd.undefined_evars env'.evd));
 	    match cstr with
-		None -> Some (hyp, hypinfo), succ occ
+		None -> Some x, succ occ
 	      | Some _ ->
 		  let (car, r, orig, dest) = hypinfo in
 		  let res = 
 		    try 
 		      Some (resolve_morphism env sigma t 
 			       (mkLambda (Name (id_of_string "x"), car, mkRel 1))
-			       (* (mkApp (Lazy.force coq_id, [| car |])) *)
-			       [| origt |] [| Some (hyp, hypinfo) |] cstr evars)
+			       (* (Termops.refresh_universes (mkApp (Lazy.force coq_id, [| car |]))) *)
+			       [| orig |] [| Some x |] cstr evars)
 		    with Not_found -> None
-		  in res, succ occ
+		  in res, succ occ)
 	  else None, succ occ
-
-      | App (m, args) ->
-	  let args', occ = 
-	    Array.fold_left 
-	      (fun (acc, occ) arg -> let res, occ = aux arg occ None in (res :: acc, occ))
-	      ([], occ) args
-	  in
-	  let res =
-	    if List.for_all (fun x -> x = None) args' then None
-	    else 
-	      let args' = Array.of_list (List.rev args') in
-		(try Some (resolve_morphism env sigma t m args args' cstr evars)
-		  with Not_found -> None)
-	  in res, occ
-
-      | Prod (_, x, b) -> 
-	  let x', occ = aux x occ None in
-	  let b', occ = aux b occ None in
-	  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)
-		with Not_found -> None)
-	  in res, occ
-
-      | _ -> None, occ
+      | None -> 
+	  match kind_of_term t with
+	    | App (m, args) ->
+		let args', occ = 
+		  Array.fold_left 
+		    (fun (acc, occ) arg -> let res, occ = aux arg occ None in (res :: acc, occ))
+		    ([], occ) args
+		in
+		let res =
+		  if List.for_all (fun x -> x = None) args' then None
+		  else 
+		    let args' = Array.of_list (List.rev args') in
+		      (try Some (resolve_morphism env sigma t m args args' cstr evars)
+			with Not_found -> None)
+		in res, occ
+		  
+	    | Prod (_, x, b) -> 
+		let x', occ = aux x occ None in
+		let b', occ = aux b occ None in
+		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)
+		      with Not_found -> None)
+		in res, occ
+		  
+	    | _ -> None, occ
   in aux concl 1 cstr
-
-let decompose_setoid_eqhyp gl env sigma c left2right t = 
-  let (c, (car, rel, x, y) as res) =
-    match kind_of_term t with
-	(*     | App (equiv, [| a; r; s; x; y |]) -> *)
-	(* 	if dir then (c, (a, r, s, x, y)) *)
-	(* 	else (c, (a, r, s, y, x)) *)
-      | App (r, args) when Array.length args >= 2 -> 
-	  let relargs, args = array_chop (Array.length args - 2) args in
-	  let rel = mkApp (r, relargs) in
-	  let typ = pf_type_of gl rel in
-	    (if isArity typ then
-	      let (ctx, ar) = destArity typ in
-		(match ctx with
-		    [ (_, None, sx) ; (_, None, sy) ] when eq_constr sx sy -> 
-		      (c, (sx, rel, args.(0), args.(1)))
-		  | _ -> error "Only binary relations are supported")
-	      else error "Not a relation")
-      | _ -> error "Not a relation"
-  in
-    if left2right then res
-    else
-      try (mkApp (symmetric_proof env car rel, [| x ; y ; c |]), (car, rel, y, x))
-      with Not_found ->
-	(c, (car, mkApp (Lazy.force inverse, [| car ; rel |]), y, x))
+    
+(* Adapted from setoid_replace. *)
+
+let decompose_setoid_eqhyp gl c left2right =
+  let ctype = pf_type_of gl c in
+  let eqclause  = Clenv.make_clenv_binding gl (c,ctype) Rawterm.NoBindings in
+  let (equiv, args) = decompose_app (Clenv.clenv_type eqclause) in
+  let rec split_last_two = function
+    | [c1;c2] -> [],(c1, c2)
+    | x::y::z ->
+	let l,res = split_last_two (y::z) in x::l, res
+    | _ -> error "The term provided is not an applied relation" in
+  let others, (c1,c2) = split_last_two args in
+    eqclause, mkApp (equiv, Array.of_list others), left2right, c1, c2
 
 let resolve_all_typeclasses env evd = 
   resolve_all_evars false (true, 15) env
     (fun ev evi -> Typeclasses.class_of_constr evi.Evd.evar_concl <> None) evd
     
-(* let _ =  *)
-(*   Typeclasses.solve_instanciation_problem := *)
-(*     (fun env evd ev evi -> resolve_all_typeclasses env evd, true) *)
-
-let cl_rewrite_clause c left2right occs clause gl =
-  let env = pf_env gl in
-  let sigma = project gl in
-  let hyp = pf_type_of gl c in
-  let hypt, (typ, rel, origt, newt as hypinfo) = decompose_setoid_eqhyp gl env sigma c left2right hyp in
+let cl_rewrite_clause_aux hypinfo occs clause gl =
   let concl, is_hyp = 
     match clause with
 	Some ((_, id), _) -> pf_get_hyp_typ gl id, Some id
@@ -588,23 +656,48 @@ let cl_rewrite_clause c left2right occs clause gl =
       | Some _ -> (mkProp, Lazy.force impl)
   in
   let evars = ref (Evd.create_evar_defs Evd.empty) in
-  let eq, _ = build_new gl env sigma occs origt newt hypt hypinfo concl (Some cstr) evars in
+  let env = pf_env gl in
+  let sigma = project gl in
+  let eq, _ = build_new gl env sigma occs hypinfo concl (Some cstr) evars in
     match eq with  
 	Some (p, (_, _, oldt, newt)) -> 
-	  evars := Typeclasses.resolve_typeclasses env (Evd.evars_of !evars) !evars;
-	  evars := Evarutil.nf_evar_defs !evars;
-	  let p = Evarutil.nf_isevar !evars p in
-	  let newt = Evarutil.nf_isevar !evars newt in
-	  let undef = Evd.undefined_evars !evars in
-	    tclTHEN (Refiner.tclEVARS (Evd.evars_of undef))
-	      (match is_hyp with
-	    | Some id -> Tactics.apply_in true id [p,NoBindings]
-	    | None -> 
-		let meta = Evarutil.new_meta() in
-		let term = mkApp (p, [| mkCast (mkMeta meta, DEFAULTcast, newt) |]) in
-		  refine term) gl
-      | None -> tclIDTAC gl
+	  (try 
+	      evars := Typeclasses.resolve_typeclasses env (Evd.evars_of !evars) !evars;
+	      let p = Evarutil.nf_isevar !evars p in
+	      let newt = Evarutil.nf_isevar !evars newt in
+	      let undef = Evd.undefined_evars !evars in
+	      let unfoldrefs = List.map (fun s -> [], EvalConstRef s) [destConst (Lazy.force impl)] in
+	      let rewtac, cleantac = 
+		match is_hyp with
+		  | Some id -> 
+(* 		      let meta = Evarutil.new_meta() in *)
+(* 		      let term = mkApp (p, [| mkCast (mkMeta meta, DEFAULTcast, newt) |]) in *)
+(* 		      tclTHEN *)
+(* 			(tclEVARS (evars_of clenv.evd)) *)
+		      cut_replacing id newt (fun x ->
+			refine (mkApp (p, [| mkVar id |]))),
+		      unfold_in_hyp unfoldrefs (([], id), Tacexpr.InHyp)
+		  | None -> 
+		      let meta = Evarutil.new_meta() in
+		      let term = mkApp (p, [| mkCast (mkMeta meta, DEFAULTcast, newt) |]) in
+			refine term, Tactics.unfold_in_concl unfoldrefs
+	      in
+	      let evartac = 
+		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
+	    with UserError (env, e) -> 
+	      tclFAIL 0 (str" setoid rewrite failed: unable to satisfy the rewriting constraints") gl)
+      | None -> 
+	  let (_, _, l2r, x, y) = hypinfo in
+	    raise (Pretype_errors.PretypeError (pf_env gl, Pretype_errors.NoOccurrenceFound (if l2r then x else y)))
+	      (* tclFAIL 1 (str"setoid rewrite failed") gl *)
 	  
+let cl_rewrite_clause c left2right occs clause gl =
+  let hypinfo = decompose_setoid_eqhyp gl c left2right in
+    cl_rewrite_clause_aux hypinfo occs clause gl
+
 open Genarg
 open Extraargs
 
@@ -616,6 +709,7 @@ TACTIC EXTEND class_rewrite
 | [ "clrewrite" orient(o) constr(c) ] -> [ cl_rewrite_clause c o [] None ]
 END
 
+
 let clsubstitute o c =
   let is_tac id = match kind_of_term c with Var id' when id' = id -> true | _ -> false in
     Tacticals.onAllClauses 
@@ -680,7 +774,7 @@ END
 let _ = 
   Typeclasses.solve_instanciations_problem :=
     resolve_argument_typeclasses false (true, 15)
-      
+
 TACTIC EXTEND typeclasses_eauto
 | [ "typeclasses" "eauto" debug(d) search_mode(s) depth(depth) ] -> [ fun gl ->
     let env = pf_env gl in
@@ -697,21 +791,439 @@ END
 let _ = 
   Classes.refine_ref := Refine.refine
 
-open Pretype_errors
+(* Compatibility with old Setoids *)
+  
+TACTIC EXTEND setoid_rewrite
+   [ "setoid_rewrite" orient(o) constr(c) ]
+   -> [ cl_rewrite_clause c o [] None ]
+ | [ "setoid_rewrite" orient(o) constr(c) "in" hyp(id) ] ->
+      [ cl_rewrite_clause c o [] (Some (([],id), []))]
+ | [ "setoid_rewrite" orient(o) constr(c) "at" occurences(occ) ] ->
+      [ cl_rewrite_clause c o occ None]
+ | [ "setoid_rewrite" orient(o) constr(c) "at" occurences(occ) "in" hyp(id)] ->
+      [ cl_rewrite_clause c o occ (Some (([],id), []))]
+ | [ "setoid_rewrite" orient(o) constr(c) "in" hyp(id) "at" occurences(occ)] ->
+      [ cl_rewrite_clause c o occ (Some (([],id), []))]
+END
+
+(* let solve_obligation lemma =  *)
+(*   tclTHEN (Tacinterp.interp (Tacexpr.TacAtom (dummy_loc, Tacexpr.TacAnyConstructor None))) *)
+(*     (eapply_with_bindings (Constrintern.interp_constr Evd.empty (Global.env()) lemma, NoBindings)) *)
+    
+let mkappc s l = CAppExpl (dummy_loc,(None,(Libnames.Ident (dummy_loc,id_of_string s))),l)
+
+let declare_instance a aeq n s = ((dummy_loc,Name n),Explicit,
+				  CApp (dummy_loc, (None, mkIdentC (id_of_string s)), 
+					[(a,None);(aeq,None)]))
+
+let anew_instance instance fields = new_instance [] instance fields None (fun _ -> ())
+
+let require_library dirpath =
+  let qualid = (dummy_loc, Libnames.qualid_of_dirpath (Libnames.dirpath_of_string dirpath)) in
+    Library.require_library [qualid] (Some false)
+
+let init_setoid () =
+  require_library "Coq.Setoids.Setoid"
+
+let declare_instance_refl a aeq n lemma = 
+  let instance = declare_instance a aeq (add_suffix n "_refl") "Reflexive" 
+  in anew_instance instance 
+       [((dummy_loc,id_of_string "reflexive"),[],lemma)]
+
+let declare_instance_sym a aeq n lemma = 
+  let instance = declare_instance a aeq (add_suffix n "_sym") "Symmetric" 
+  in anew_instance instance 
+       [((dummy_loc,id_of_string "symmetric"),[],lemma)]
+
+let declare_instance_trans a aeq n lemma = 
+  let instance = declare_instance a aeq (add_suffix n "_trans") "Transitive" 
+  in anew_instance instance 
+       [((dummy_loc,id_of_string "transitive"),[],lemma)]
+
+let constr_tac = Tacinterp.interp (Tacexpr.TacAtom (dummy_loc, Tacexpr.TacAnyConstructor None)) 
+
+let declare_relation a aeq n refl symm trans = 
+  init_setoid ();
+  match (refl,symm,trans) with 
+      (None, None, None) -> 
+	let instance = declare_instance a aeq n "Equivalence" 
+	in ignore(
+	  Flags.make_silent true;
+	  anew_instance instance 
+	    [((dummy_loc,id_of_string "equiv_refl"), [], CHole(dummy_loc,Some GoalEvar));
+	     ((dummy_loc,id_of_string "equiv_sym"),  [], CHole(dummy_loc,Some GoalEvar));
+	     ((dummy_loc,id_of_string "equiv_trans"),[], CHole(dummy_loc,Some GoalEvar))]);
+	  solve_nth 1 constr_tac; solve_nth 2 constr_tac; solve_nth 3 constr_tac;
+	  Flags.make_silent false; msg (Printer.pr_open_subgoals ())
+    | (Some lemma1, None, None) -> 
+	ignore (declare_instance_refl a aeq n lemma1)
+    | (None, Some lemma2, None) -> 
+	ignore (declare_instance_sym a aeq n lemma2)
+    | (None, None, Some lemma3) -> 
+	ignore (declare_instance_trans a aeq n lemma3)
+    | (Some lemma1, Some lemma2, None) -> 
+	ignore (declare_instance_refl a aeq n lemma1); 
+	ignore (declare_instance_sym a aeq n lemma2)
+    | (Some lemma1, None, Some lemma3) -> 
+	let lemma_refl = declare_instance_refl a aeq n lemma1 in
+	let lemma_trans = declare_instance_trans a aeq n lemma3 in
+	let instance = declare_instance a aeq n "PreOrder" 
+	in ignore(
+	    anew_instance instance 
+	      [((dummy_loc,id_of_string "preorder_refl"), [], mkIdentC lemma_refl);
+	       ((dummy_loc,id_of_string "preorder_trans"),[], mkIdentC lemma_trans)])
+    | (None, Some lemma2, Some lemma3) -> 
+	let lemma_sym = declare_instance_sym a aeq n lemma2 in
+	let lemma_trans = declare_instance_trans a aeq n lemma3 in
+	let instance = declare_instance a aeq n "PER" 
+	in ignore(
+	    anew_instance instance 
+	      [((dummy_loc,id_of_string "per_sym"),  [], mkIdentC lemma_sym);
+	       ((dummy_loc,id_of_string "per_trans"),[], mkIdentC lemma_trans)])
+     | (Some lemma1, Some lemma2, Some lemma3) -> 
+	let lemma_refl = declare_instance_refl a aeq n lemma1 in 
+	let lemma_sym = declare_instance_sym a aeq n lemma2 in
+	let lemma_trans = declare_instance_trans a aeq n lemma3 in
+	let instance = declare_instance a aeq n "Equivalence" 
+	in ignore(
+	    anew_instance instance 
+	      [((dummy_loc,id_of_string "equiv_refl"), [], mkIdentC lemma_refl);
+	       ((dummy_loc,id_of_string "equiv_sym"),  [], mkIdentC lemma_sym);
+	       ((dummy_loc,id_of_string "equiv_trans"),[], mkIdentC lemma_trans)])
+
+VERNAC COMMAND EXTEND AddRelation
+    [ "Add" "Relation" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1) 
+	"symmetry" "proved" "by" constr(lemma2) "as" ident(n) ] ->
+      [ declare_relation a aeq n (Some lemma1) (Some lemma2) None ]
+  | [ "Add" "Relation" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1)  
+	"as" ident(n) ] ->
+      [ declare_relation a aeq n (Some lemma1) None None ]
+  | [ "Add" "Relation" constr(a) constr(aeq)  "as" ident(n) ] -> 
+      [ declare_relation a aeq n None None None ]
+END
+
+VERNAC COMMAND EXTEND AddRelation2
+    [ "Add" "Relation" constr(a) constr(aeq) "symmetry" "proved" "by" constr(lemma2) 
+      "as" ident(n) ] ->
+      [ declare_relation a aeq n None (Some lemma2) None ]
+  | [ "Add" "Relation" constr(a) constr(aeq) "symmetry" "proved" "by" constr(lemma2) "transitivity" "proved" "by" constr(lemma3)  "as" ident(n) ] ->
+      [ declare_relation a aeq n None (Some lemma2) (Some lemma3) ]
+END
+
+VERNAC COMMAND EXTEND AddRelation3
+    [ "Add" "Relation" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1) 
+      "transitivity" "proved" "by" constr(lemma3) "as" ident(n) ] ->
+      [ declare_relation a aeq n (Some lemma1) None (Some lemma3) ]
+  | [ "Add" "Relation" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1) 
+      "symmetry" "proved" "by" constr(lemma2) "transitivity" "proved" "by" constr(lemma3) 
+      "as" ident(n) ] ->
+      [ declare_relation a aeq n (Some lemma1) (Some lemma2) (Some lemma3) ] 
+  | [ "Add" "Relation" constr(a) constr(aeq) "transitivity" "proved" "by" constr(lemma3)
+	"as" ident(n) ] ->  
+      [ declare_relation a aeq n None None (Some lemma3) ] 
+END
+
+let mk_qualid s =
+  Libnames.Qualid (dummy_loc, Libnames.qualid_of_string s)
 
-let typeclass_error e = 
-  match e with
-    | UnsolvableImplicit (evi, (InternalHole | ImplicitArg _)) ->
-	(match class_of_constr evi.evar_concl with
-	    Some c -> true
-	  | None -> false)
-    | _ -> false
+let cHole = CHole (dummy_loc, None)
+
+open Entries
+open Libnames
+
+let respect_projection r ty =
+  let ctx, inst = Sign.decompose_prod_assum ty in
+  let mor, args = destApp inst in
+  let instarg = mkApp (r, rel_vect 0 (List.length ctx)) in
+  let app = mkApp (mkConst (Lazy.force respect_proj), 
+		  Array.append args [| instarg |]) in
+    it_mkLambda_or_LetIn app ctx
+      
+let declare_projection n instance_id r =
+  let ty = Global.type_of_global r in
+  let c = constr_of_global r in
+  let term = respect_projection c ty in
+  let typ = Typing.type_of (Global.env ()) Evd.empty term in
+  let typ =
+    let n = 
+      let rec aux t = 
+	match kind_of_term t with
+	    App (f, [| a ; rel; a'; rel' |]) when eq_constr f (Lazy.force respectful) -> 
+	      succ (aux rel')
+	  | _ -> 0
+      in
+      let init = 
+	match kind_of_term typ with
+	    App (f, args) when eq_constr f (Lazy.force respectful) -> 
+	      mkApp (f, fst (array_chop (Array.length args - 2) args))
+	  | _ -> typ
+      in aux init
+    in
+    let ctx,ccl = Reductionops.decomp_n_prod (Global.env()) Evd.empty (3 * n) typ
+    in it_mkProd_or_LetIn ccl ctx 
+  in
+  let cst = 
+    { const_entry_body = term;
+      const_entry_type = Some typ;
+      const_entry_opaque = false;
+      const_entry_boxed = false }
+  in
+    ignore(Declare.declare_constant n (Entries.DefinitionEntry cst, Decl_kinds.IsDefinition Decl_kinds.Definition))
+      
+(*   try  *)
+(*     Command.declare_definition n (Decl_kinds.Local, false, Decl_kinds.Definition) [] None  *)
+(*       (CAppExpl (dummy_loc,  *)
+(* 		(None, mk_qualid "Coq.Classes.Morphisms.respect"), *)
+(* 		[ cHole; cHole; cHole; mkIdentC instance_id ])) *)
+(*       None (fun _ _ -> ()) *)
+(*   with _ -> () *)
+    
+let build_morphism_signature m =
+  let env = Global.env () in
+  let m = Constrintern.interp_constr Evd.empty env m in
+  let t = Typing.type_of env Evd.empty m in
+  let isevars = ref (Evd.create_evar_defs Evd.empty) in
+  let cstrs = 
+    let rec aux t = 
+      match kind_of_term t with
+	| Prod (na, a, b) -> 
+	    None :: aux b
+	| _ -> [None]
+    in aux t
+  in
+  let sig_, evars = build_signature isevars env t cstrs snd in
+  let _ = List.iter 
+    (fun (ty, relty) -> 
+      let equiv = mkApp (Lazy.force equivalence, [| ty; relty |]) in
+	ignore(Evarutil.e_new_evar isevars env equiv))
+    evars
+  in
+  let morph = 
+    mkApp (mkInd (Lazy.force morphism_class).cl_impl, [| t; sig_; m |])
+  in
+(*   let morphev = Evarutil.e_new_evar isevars env morph in *)
+  let evd = resolve_all_evars_once false (true, 15) env
+    (fun x evi -> class_of_constr evi.Evd.evar_concl <> None) !isevars in
+    Evarutil.nf_isevar evd morph
+
+let default_morphism sign m =
+  let env = Global.env () in
+  let isevars = ref (Evd.create_evar_defs Evd.empty) in
+  let t = Typing.type_of env Evd.empty m in
+  let sign, evars = 
+    build_signature isevars env t sign (fun (ty, rel) -> rel)
+  in
+  let morph = 
+    mkApp (mkInd (Lazy.force morphism_class).cl_impl, [| t; sign; m |])
+  in
+  let mor = resolve_one_typeclass env morph in
+    mor, respect_projection mor morph
+    	  
+let unfold_respectful = lazy (Tactics.unfold_in_concl [[], EvalConstRef (destConst (Lazy.force respectful))])
+
+let ($) g f = fun x -> g (f x)
+
+VERNAC COMMAND EXTEND AddSetoid1
+   [ "Add" "Setoid" constr(a) constr(aeq) constr(t) "as" ident(n) ] ->
+     [	init_setoid ();
+	let lemma_refl = declare_instance_refl a aeq n (mkappc "Seq_refl" [a;aeq;t]) in 
+	let lemma_sym = declare_instance_sym a aeq n (mkappc "Seq_sym" [a;aeq;t]) in
+	let lemma_trans = declare_instance_trans a aeq n (mkappc "Seq_trans" [a;aeq;t])  in
+	let instance = declare_instance a aeq n "Equivalence"
+	in ignore(
+	    anew_instance instance
+	      [((dummy_loc,id_of_string "equiv_refl"), [], mkIdentC lemma_refl);
+	       ((dummy_loc,id_of_string "equiv_sym"),  [], mkIdentC lemma_sym);
+	       ((dummy_loc,id_of_string "equiv_trans"),[], mkIdentC lemma_trans)])]
+  | [ "Add" "Morphism" constr(m) ":" ident(n) ] ->
+      [ init_setoid ();
+	let instance_id = add_suffix n "_Morphism" in
+	let instance = build_morphism_signature m in
+	  if Lib.is_modtype () then 
+	    let cst = Declare.declare_internal_constant instance_id
+	      (Entries.ParameterEntry (instance,false), Decl_kinds.IsAssumption Decl_kinds.Logical)
+	    in
+	      add_instance { is_class = Lazy.force morphism_class ; is_pri = None; is_impl = cst };
+	      declare_projection n instance_id (ConstRef cst)
+	  else
+	    let kind = Decl_kinds.Global, Decl_kinds.DefinitionBody Decl_kinds.Instance in
+	      Flags.silently 
+		(fun () ->
+		  Command.start_proof instance_id kind instance 
+		    (fun _ -> function
+			Libnames.ConstRef cst -> 
+			  add_instance { is_class = Lazy.force morphism_class ; is_pri = None; is_impl = cst };
+			  declare_projection n instance_id (ConstRef cst)
+		      | _ -> assert false);
+		  Pfedit.by (Tacinterp.interp <:tactic<add_morphism_tactic>>)) ();
+	      Flags.if_verbose (fun x -> msg (Printer.pr_open_subgoals x)) () ]
+
+  | [ "Add" "Morphism" constr(m) "with" "signature" lconstr(s) "as" ident(n) ] ->
+      [ init_setoid ();
+	let instance_id = add_suffix n "_Morphism" in
+	let instance = 
+	  ((dummy_loc,Name instance_id), Implicit,
+	  CApp (dummy_loc, (None, mkRefC 
+	    (Qualid (dummy_loc, Libnames.qualid_of_string "Coq.Classes.Morphisms.Morphism"))), 
+	       [(s,None);(m,None)]))
+	in
+	  if Lib.is_modtype () then (context ~hook:(fun r -> declare_projection n instance_id r) [ instance ])
+	  else (
+	    Flags.silently 
+	      (fun () ->
+		ignore(new_instance [] instance [] None (fun cst -> declare_projection n instance_id (ConstRef cst)));
+		Pfedit.by (Tacinterp.interp <:tactic<add_morphism_tactic>>)) ();
+	    Flags.if_verbose (msg $ Printer.pr_open_subgoals) ())
+      ]
+END
+
+(** Bind to "rewrite" too *)
+
+(** Taken from original setoid_replace, to emulate the old rewrite semantics where
+    lemmas are first instantiated once and then rewrite proceeds. *)
+
+let unification_rewrite l2r c1 c2 cl but gl = 
+  let (env',c') =
+    try
+      (* ~flags:(false,true) to allow to mark occurences that must not be
+         rewritten simply by replacing them with let-defined definitions
+         in the context *)
+      Unification.w_unify_to_subterm ~flags:rewrite_unif_flags (pf_env gl) ((if l2r then c1 else c2),but) cl.evd
+    with
+	Pretype_errors.PretypeError _ ->
+	  (* ~flags:(true,true) to make Ring work (since it really
+             exploits conversion) *)
+	  Unification.w_unify_to_subterm ~flags:rewrite2_unif_flags
+	    (pf_env gl) ((if l2r then c1 else c2),but) cl.evd
+  in
+  let cl' = {cl with evd = env' } in
+  let c1 = Clenv.clenv_nf_meta cl' c1 
+  and c2 = Clenv.clenv_nf_meta cl' c2 in
+    cl', Clenv.clenv_value cl', l2r, c1, c2
+
+let get_hyp gl c clause l2r = 
+  match kind_of_term (pf_type_of gl c) with
+      Prod _ -> 
+	let cl, rel, _, c1, c2 = decompose_setoid_eqhyp gl c l2r in
+	let but = match clause with Some id -> pf_get_hyp_typ gl id | None -> pf_concl gl in
+	  unification_rewrite l2r c1 c2 cl but gl 
+    | _ -> decompose_setoid_eqhyp gl c l2r
 	
-let class_apply c = 
-  try Tactics.apply_with_ebindings c
-  with PretypeError (env, e) when typeclass_error e -> 
-    tclFAIL 1 (str"typeclass resolution failed")
+let general_s_rewrite l2r c ~new_goals gl =
+  let hypinfo = get_hyp gl c None l2r in
+    cl_rewrite_clause_aux hypinfo [] None gl
 
-TACTIC EXTEND class_apply
-| [ "class_apply" constr_with_bindings(t) ] -> [ class_apply t ]
+let general_s_rewrite_in id l2r c ~new_goals gl =
+  let hypinfo = get_hyp gl c (Some id) l2r in
+    cl_rewrite_clause_aux hypinfo [] (Some (([],id), [])) gl
+    
+let general_s_rewrite_clause = function
+  | None -> general_s_rewrite
+  | Some id -> general_s_rewrite_in id
+
+let _ = Equality.register_general_setoid_rewrite_clause general_s_rewrite_clause
+
+(* [setoid_]{reflexivity,symmetry,transitivity} tactics *)
+
+let relation_of_constr c = 
+  match kind_of_term c with
+    | App (f, args) when Array.length args >= 2 -> 
+	let relargs, args = array_chop (Array.length args - 2) args in
+	  mkApp (f, relargs), args
+    | _ -> error "Not an applied relation"
+
+let setoid_reflexivity gl =
+  let env = pf_env gl in
+  let rel, args = relation_of_constr (pf_concl gl) in
+    try
+      apply (reflexive_proof env (pf_type_of gl args.(0)) rel) gl
+    with Not_found -> 
+      tclFAIL 0 (str" The relation " ++ Printer.pr_constr_env env rel ++ str" is not a declared reflexive relation")
+	gl
+
+let setoid_symmetry gl =
+  let env = pf_env gl in
+  let rel, args = relation_of_constr (pf_concl gl) in
+    try
+      apply (symmetric_proof env (pf_type_of gl args.(0)) rel) gl
+    with Not_found -> 
+      tclFAIL 0 (str" The relation " ++ Printer.pr_constr_env env rel ++ str" is not a declared symmetric relation")
+	gl
+	
+let setoid_transitivity c gl =
+  let env = pf_env gl in
+  let rel, args = relation_of_constr (pf_concl gl) in
+    try
+      apply_with_bindings
+	((transitive_proof env (pf_type_of gl args.(0)) rel),
+	Rawterm.ExplicitBindings [ dummy_loc, Rawterm.NamedHyp (id_of_string "y"), c ]) gl
+    with Not_found -> 
+      tclFAIL 0
+	(str" The relation " ++ Printer.pr_constr_env env rel ++ str" is not a declared transitive relation") gl
+	
+let setoid_symmetry_in id gl =
+  let ctype = pf_type_of gl (mkVar id) in
+  let binders,concl = Sign.decompose_prod_assum ctype in
+  let (equiv, args) = decompose_app concl in
+  let rec split_last_two = function
+    | [c1;c2] -> [],(c1, c2)
+    | x::y::z -> let l,res = split_last_two (y::z) in x::l, res
+    | _ -> error "The term provided is not an equivalence" 
+  in
+  let others,(c1,c2) = split_last_two args in
+  let he,c1,c2 =  mkApp (equiv, Array.of_list others),c1,c2 in
+  let new_hyp' =  mkApp (he, [| c2 ; c1 |]) in
+  let new_hyp = it_mkProd_or_LetIn new_hyp'  binders in
+    tclTHENS (cut new_hyp)
+      [ intro_replacing id;
+	tclTHENLIST [ intros; setoid_symmetry; apply (mkVar id); Tactics.assumption ] ]
+      gl
+
+let _ = Tactics.register_setoid_reflexivity setoid_reflexivity
+let _ = Tactics.register_setoid_symmetry setoid_symmetry
+let _ = Tactics.register_setoid_symmetry_in setoid_symmetry_in
+let _ = Tactics.register_setoid_transitivity setoid_transitivity
+
+TACTIC EXTEND setoid_symmetry
+   [ "setoid_symmetry" ] -> [ setoid_symmetry ]
+ | [ "setoid_symmetry" "in" hyp(n) ] -> [ setoid_symmetry_in n ]
+END
+
+TACTIC EXTEND setoid_reflexivity
+   [ "setoid_reflexivity" ] -> [ setoid_reflexivity ]
+END
+
+TACTIC EXTEND setoid_transitivity
+   [ "setoid_transitivity" constr(t) ] -> [ setoid_transitivity t ]
 END
+
+(* open Pretype_errors *)
+
+(* let typeclass_error e = *)
+(*   match e with *)
+(*     | UnsolvableImplicit (evi, (InternalHole | ImplicitArg _)) -> *)
+(* 	(match class_of_constr evi.evar_concl with *)
+(* 	    Some c -> true *)
+(* 	  | None -> false) *)
+(*     | _ -> false *)
+	
+(* let class_apply c = *)
+(*   try Tactics.apply_with_ebindings c *)
+(*   with PretypeError (env, e) when typeclass_error e -> *)
+(*     tclFAIL 1 (str"typeclass resolution failed") *)
+
+(* TACTIC EXTEND class_apply *)
+(*     | [ "class_apply" constr_with_bindings(t) ] -> [ class_apply t ] *)
+(* END *)
+
+(* let default_morphism ?(filter=fun _ -> true) m = *)
+(*   match List.filter filter (morphism_table_find m) with *)
+(*       [] -> raise Not_found *)
+(*     | m1::ml -> *)
+(*         if ml <> [] then *)
+(*           Flags.if_warn msg_warning *)
+(*             (strbrk "There are several morphisms associated to \"" ++ *)
+(*             pr_lconstr m ++ strbrk "\". Morphism " ++ prmorphism m m1 ++ *)
+(*             strbrk " is randomly chosen."); *)
+(*         relation_morphism_of_constr_morphism m1 *)
+
diff --git a/tactics/equality.ml b/tactics/equality.ml
index b6c3acface..93b555b34d 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -51,10 +51,6 @@ open Indrec
    -- Eduardo (19/8/97)
 *)
 
-let general_s_rewrite_clause = function
-  | None -> general_s_rewrite
-  | Some id -> general_s_rewrite_in id
-
 (* Ad hoc asymmetric general_elim_clause *)
 let general_elim_clause with_evars cls c elim = match cls with
   | None ->
@@ -81,6 +77,13 @@ let elimination_sort_of_clause = function
    else back to the old approach
 *)
 
+let general_s_rewrite_clause = function
+  | None -> general_s_rewrite
+  | Some id -> general_s_rewrite_in id
+
+let general_setoid_rewrite_clause = ref general_s_rewrite_clause
+let register_general_setoid_rewrite_clause = (:=) general_setoid_rewrite_clause
+
 let general_rewrite_ebindings_clause cls lft2rgt (c,l) with_evars gl =
   let ctype = pf_apply get_type_of gl c in 
   (* A delta-reduction would be here too strong, since it would 
@@ -88,7 +91,7 @@ let general_rewrite_ebindings_clause cls lft2rgt (c,l) with_evars gl =
   let t = snd (decompose_prod (whd_betaiotazeta ctype)) in 
   let head = if isApp t then fst (destApp t) else t in 
     if relation_table_mem head && l = NoBindings then 
-      general_s_rewrite_clause cls lft2rgt c [] gl
+      !general_setoid_rewrite_clause cls lft2rgt c [] gl
     else 
       (* Original code. In particular, [splay_prod] performs delta-reduction. *)
       let env = pf_env gl in
@@ -97,7 +100,7 @@ let general_rewrite_ebindings_clause cls lft2rgt (c,l) with_evars gl =
 	match match_with_equation t with
 	  | None -> 
 	      if l = NoBindings
-	      then general_s_rewrite_clause cls lft2rgt c [] gl
+	      then !general_setoid_rewrite_clause cls lft2rgt c [] gl
 	      else error "The term provided does not end with an equation" 
 	  | Some (hdcncl,_) -> 
               let hdcncls = string_of_inductive hdcncl in 
@@ -109,7 +112,13 @@ let general_rewrite_ebindings_clause cls lft2rgt (c,l) with_evars gl =
 		with Not_found ->
 		  error ("Cannot find rewrite principle "^rwr_thm)
               in 
-		general_elim_clause with_evars cls (c,l) (elim,NoBindings) gl
+		try general_elim_clause with_evars cls (c,l) (elim,NoBindings) gl
+		with e -> 
+		  let eq = build_coq_eq () in
+		    if not (eq_constr eq head) then
+		      try !general_setoid_rewrite_clause cls lft2rgt c [] gl
+		      with _ -> raise e
+		    else raise e
 
 let general_rewrite_ebindings = 
   general_rewrite_ebindings_clause None
diff --git a/tactics/equality.mli b/tactics/equality.mli
index 475304fb6c..846487f964 100644
--- a/tactics/equality.mli
+++ b/tactics/equality.mli
@@ -41,6 +41,10 @@ val rewriteRL   : constr  -> tactic
 
 (* Warning: old [general_rewrite_in] is now [general_rewrite_bindings_in] *)
 
+val register_general_setoid_rewrite_clause :
+  (identifier option ->
+    bool -> constr -> new_goals:constr list -> tactic) -> unit
+
 val general_rewrite_bindings_in :
   bool -> identifier -> constr with_bindings -> evars_flag -> tactic
 val general_rewrite_in          :
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index 0fff16cf92..dd0fecc82b 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -150,82 +150,82 @@ let refine_tac = h_refine
 
 open Setoid_replace
 
-TACTIC EXTEND setoid_replace
-   [ "setoid_replace" constr(c1) "with" constr(c2) by_arg_tac(tac)] ->
-     [ setoid_replace  (Option.map Tacinterp.eval_tactic tac) None c1 c2 ~new_goals:[] ]
- | [ "setoid_replace" constr(c1) "with" constr(c2) "using" "relation" constr(rel) by_arg_tac(tac)] ->
-     [ setoid_replace  (Option.map Tacinterp.eval_tactic tac) (Some rel) c1 c2 ~new_goals:[] ]
- | [ "setoid_replace" constr(c1) "with" constr(c2) "generate" "side" "conditions" constr_list(l) by_arg_tac(tac) ] ->
-     [ setoid_replace  (Option.map Tacinterp.eval_tactic tac) None c1 c2 ~new_goals:l ]
- | [ "setoid_replace" constr(c1) "with" constr(c2) "using" "relation" constr(rel) "generate" "side" "conditions" constr_list(l) by_arg_tac(tac) ] ->
-     [ setoid_replace  (Option.map Tacinterp.eval_tactic tac) (Some rel) c1 c2 ~new_goals:l ]
- | [ "setoid_replace" constr(c1) "with" constr(c2) "in" hyp(h) by_arg_tac(tac) ] ->
-     [ setoid_replace_in  (Option.map Tacinterp.eval_tactic tac) h None c1 c2 ~new_goals:[] ]
- | [ "setoid_replace" constr(c1) "with" constr(c2) "in" hyp(h) "using" "relation" constr(rel) by_arg_tac(tac)] ->
-     [ setoid_replace_in  (Option.map Tacinterp.eval_tactic tac) h (Some rel) c1 c2 ~new_goals:[] ]
- | [ "setoid_replace" constr(c1) "with" constr(c2) "in" hyp(h) "generate" "side" "conditions" constr_list(l) by_arg_tac(tac)] ->
-     [ setoid_replace_in  (Option.map Tacinterp.eval_tactic tac) h None c1 c2 ~new_goals:l ]
- | [ "setoid_replace" constr(c1) "with" constr(c2) "in" hyp(h) "using" "relation" constr(rel) "generate" "side" "conditions" constr_list(l) by_arg_tac(tac)] ->
-     [ setoid_replace_in  (Option.map Tacinterp.eval_tactic tac) h (Some rel) c1 c2 ~new_goals:l ]
-END
-
-TACTIC EXTEND setoid_rewrite
-   [ "setoid_rewrite" orient(b) constr(c) ]
-   -> [ general_s_rewrite b c ~new_goals:[] ]
- | [ "setoid_rewrite" orient(b) constr(c) "generate" "side" "conditions" constr_list(l) ]
-   -> [ general_s_rewrite b c ~new_goals:l ]
- | [ "setoid_rewrite" orient(b) constr(c) "in" hyp(h) ] ->
-      [ general_s_rewrite_in h b c ~new_goals:[] ]
- | [ "setoid_rewrite" orient(b) constr(c) "in" hyp(h) "generate" "side" "conditions" constr_list(l) ] ->
-      [ general_s_rewrite_in h b c ~new_goals:l ]
-END
-
-VERNAC COMMAND EXTEND AddSetoid1
-  [ "Add" "Setoid" constr(a) constr(aeq) constr(t) "as" ident(n) ] ->
-   [ add_setoid n a aeq t ]
-| [ "Add" "Morphism" constr(m) ":" ident(n) ] ->
-   [ new_named_morphism n m None ]
-| [ "Add" "Morphism" constr(m) "with" "signature" morphism_signature(s) "as" ident(n) ] ->
-   [ new_named_morphism n m (Some s)]
-END
-
-VERNAC COMMAND EXTEND AddRelation1
-  [ "Add" "Relation" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(t) "symmetry" "proved" "by" constr(t') "as" ident(n) ] ->
-   [ add_relation n a aeq (Some t) (Some t') None ]
-| [ "Add" "Relation" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(t)  "as" ident(n) ] ->
-   [ add_relation n a aeq (Some t) None None ]
-| [ "Add" "Relation" constr(a) constr(aeq)  "as" ident(n) ] ->
-   [ add_relation n a aeq None None None ]
-END
-
-VERNAC COMMAND EXTEND AddRelation2
-  [ "Add" "Relation" constr(a) constr(aeq) "symmetry" "proved" "by" constr(t') "as" ident(n) ] ->
-   [ add_relation n a aeq None (Some t') None ]
-| [ "Add" "Relation" constr(a) constr(aeq) "symmetry" "proved" "by" constr(t') "transitivity" "proved" "by" constr(t'')  "as" ident(n) ] ->
-   [ add_relation n a aeq None (Some t') (Some t'') ]
-END
-
-VERNAC COMMAND EXTEND AddRelation3
-  [ "Add" "Relation" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(t) "transitivity" "proved" "by" constr(t') "as" ident(n) ] ->
-   [ add_relation n a aeq (Some t) None (Some t') ]
-| [ "Add" "Relation" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(t) "symmetry" "proved" "by" constr(t') "transitivity" "proved" "by" constr(t'') "as" ident(n) ] ->
-   [ add_relation n a aeq (Some t) (Some t') (Some t'') ]
-| [ "Add" "Relation" constr(a) constr(aeq) "transitivity" "proved" "by" constr(t) "as" ident(n) ] ->
-   [ add_relation n a aeq None None (Some t) ]
-END
-
-TACTIC EXTEND setoid_symmetry
-   [ "setoid_symmetry" ] -> [ setoid_symmetry ]
- | [ "setoid_symmetry" "in" hyp(n) ] -> [ setoid_symmetry_in n ]
-END
-
-TACTIC EXTEND setoid_reflexivity
-   [ "setoid_reflexivity" ] -> [ setoid_reflexivity ]
-END
-
-TACTIC EXTEND setoid_transitivity
-   [ "setoid_transitivity" constr(t) ] -> [ setoid_transitivity t ]
-END
+(* TACTIC EXTEND setoid_replace *)
+(*    [ "setoid_replace" constr(c1) "with" constr(c2) by_arg_tac(tac)] -> *)
+(*      [ setoid_replace  (Option.map Tacinterp.eval_tactic tac) None c1 c2 ~new_goals:[] ] *)
+(*  | [ "setoid_replace" constr(c1) "with" constr(c2) "using" "relation" constr(rel) by_arg_tac(tac)] -> *)
+(*      [ setoid_replace  (Option.map Tacinterp.eval_tactic tac) (Some rel) c1 c2 ~new_goals:[] ] *)
+(*  | [ "setoid_replace" constr(c1) "with" constr(c2) "generate" "side" "conditions" constr_list(l) by_arg_tac(tac) ] -> *)
+(*      [ setoid_replace  (Option.map Tacinterp.eval_tactic tac) None c1 c2 ~new_goals:l ] *)
+(*  | [ "setoid_replace" constr(c1) "with" constr(c2) "using" "relation" constr(rel) "generate" "side" "conditions" constr_list(l) by_arg_tac(tac) ] -> *)
+(*      [ setoid_replace  (Option.map Tacinterp.eval_tactic tac) (Some rel) c1 c2 ~new_goals:l ] *)
+(*  | [ "setoid_replace" constr(c1) "with" constr(c2) "in" hyp(h) by_arg_tac(tac) ] -> *)
+(*      [ setoid_replace_in  (Option.map Tacinterp.eval_tactic tac) h None c1 c2 ~new_goals:[] ] *)
+(*  | [ "setoid_replace" constr(c1) "with" constr(c2) "in" hyp(h) "using" "relation" constr(rel) by_arg_tac(tac)] -> *)
+(*      [ setoid_replace_in  (Option.map Tacinterp.eval_tactic tac) h (Some rel) c1 c2 ~new_goals:[] ] *)
+(*  | [ "setoid_replace" constr(c1) "with" constr(c2) "in" hyp(h) "generate" "side" "conditions" constr_list(l) by_arg_tac(tac)] -> *)
+(*      [ setoid_replace_in  (Option.map Tacinterp.eval_tactic tac) h None c1 c2 ~new_goals:l ] *)
+(*  | [ "setoid_replace" constr(c1) "with" constr(c2) "in" hyp(h) "using" "relation" constr(rel) "generate" "side" "conditions" constr_list(l) by_arg_tac(tac)] -> *)
+(*      [ setoid_replace_in  (Option.map Tacinterp.eval_tactic tac) h (Some rel) c1 c2 ~new_goals:l ] *)
+(* END *)
+
+(* TACTIC EXTEND setoid_rewrite *)
+(*    [ "setoid_rewrite" orient(b) constr(c) ] *)
+(*    -> [ general_s_rewrite b c ~new_goals:[] ] *)
+(*  | [ "setoid_rewrite" orient(b) constr(c) "generate" "side" "conditions" constr_list(l) ] *)
+(*    -> [ general_s_rewrite b c ~new_goals:l ] *)
+(*  | [ "setoid_rewrite" orient(b) constr(c) "in" hyp(h) ] -> *)
+(*       [ general_s_rewrite_in h b c ~new_goals:[] ] *)
+(*  | [ "setoid_rewrite" orient(b) constr(c) "in" hyp(h) "generate" "side" "conditions" constr_list(l) ] -> *)
+(*       [ general_s_rewrite_in h b c ~new_goals:l ] *)
+(* END *)
+
+(* VERNAC COMMAND EXTEND AddSetoid1 *)
+(*   [ "Add" "Setoid" constr(a) constr(aeq) constr(t) "as" ident(n) ] -> *)
+(*    [ add_setoid n a aeq t ] *)
+(* | [ "Add" "Morphism" constr(m) ":" ident(n) ] -> *)
+(*    [ new_named_morphism n m None ] *)
+(* | [ "Add" "Morphism" constr(m) "with" "signature" morphism_signature(s) "as" ident(n) ] -> *)
+(*    [ new_named_morphism n m (Some s)] *)
+(* END *)
+
+(* VERNAC COMMAND EXTEND AddRelation1 *)
+(*   [ "Add" "Relation" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(t) "symmetry" "proved" "by" constr(t') "as" ident(n) ] -> *)
+(*    [ add_relation n a aeq (Some t) (Some t') None ] *)
+(* | [ "Add" "Relation" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(t)  "as" ident(n) ] -> *)
+(*    [ add_relation n a aeq (Some t) None None ] *)
+(* | [ "Add" "Relation" constr(a) constr(aeq)  "as" ident(n) ] -> *)
+(*    [ add_relation n a aeq None None None ] *)
+(* END *)
+
+(* VERNAC COMMAND EXTEND AddRelation2 *)
+(*   [ "Add" "Relation" constr(a) constr(aeq) "symmetry" "proved" "by" constr(t') "as" ident(n) ] -> *)
+(*    [ add_relation n a aeq None (Some t') None ] *)
+(* | [ "Add" "Relation" constr(a) constr(aeq) "symmetry" "proved" "by" constr(t') "transitivity" "proved" "by" constr(t'')  "as" ident(n) ] -> *)
+(*    [ add_relation n a aeq None (Some t') (Some t'') ] *)
+(* END *)
+
+(* VERNAC COMMAND EXTEND AddRelation3 *)
+(*   [ "Add" "Relation" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(t) "transitivity" "proved" "by" constr(t') "as" ident(n) ] -> *)
+(*    [ add_relation n a aeq (Some t) None (Some t') ] *)
+(* | [ "Add" "Relation" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(t) "symmetry" "proved" "by" constr(t') "transitivity" "proved" "by" constr(t'') "as" ident(n) ] -> *)
+(*    [ add_relation n a aeq (Some t) (Some t') (Some t'') ] *)
+(* | [ "Add" "Relation" constr(a) constr(aeq) "transitivity" "proved" "by" constr(t) "as" ident(n) ] -> *)
+(*    [ add_relation n a aeq None None (Some t) ] *)
+(* END *)
+
+(* TACTIC EXTEND setoid_symmetry *)
+(*    [ "setoid_symmetry" ] -> [ setoid_symmetry ] *)
+(*  | [ "setoid_symmetry" "in" hyp(n) ] -> [ setoid_symmetry_in n ] *)
+(* END *)
+
+(* TACTIC EXTEND setoid_reflexivity *)
+(*    [ "setoid_reflexivity" ] -> [ setoid_reflexivity ] *)
+(* END *)
+
+(* TACTIC EXTEND setoid_transitivity *)
+(*    [ "setoid_transitivity" constr(t) ] -> [ setoid_transitivity t ] *)
+(* END *)
 
 (* Inversion lemmas (Leminv) *)
 
diff --git a/tactics/setoid_replace.ml b/tactics/setoid_replace.ml
index 0214a940cb..7e7b81ebf1 100644
--- a/tactics/setoid_replace.ml
+++ b/tactics/setoid_replace.ml
@@ -2017,7 +2017,3 @@ let setoid_transitivity c gl =
   Optimize -> transitivity_red true c gl
 ;;
 
-Tactics.register_setoid_reflexivity setoid_reflexivity;;
-Tactics.register_setoid_symmetry setoid_symmetry;;
-Tactics.register_setoid_symmetry_in setoid_symmetry_in;;
-Tactics.register_setoid_transitivity setoid_transitivity;;
diff --git a/test-suite/typeclasses/clrewrite.v b/test-suite/typeclasses/clrewrite.v
index 5c56a0daf7..2978fda266 100644
--- a/test-suite/typeclasses/clrewrite.v
+++ b/test-suite/typeclasses/clrewrite.v
@@ -108,4 +108,4 @@ Section Trans.
     apply H0.
   Qed.
 
-End Trans.
\ No newline at end of file
+End Trans.
diff --git a/theories/Classes/Equivalence.v b/theories/Classes/Equivalence.v
index bf26021800..da302ea9d0 100644
--- a/theories/Classes/Equivalence.v
+++ b/theories/Classes/Equivalence.v
@@ -101,6 +101,31 @@ Tactic Notation "setoid_replace" constr(x) "with" constr(y) "in" hyp(id)
 Tactic Notation "setoid_replace" constr(x) "with" constr(y) "in" hyp(id)
   "using" "relation" constr(rel) "by" tactic(t) :=
   setoidreplacein (rel x y) id ltac:t.
+
+
+Ltac red_subst_eq_morphism concl :=
+  match concl with
+    | @Logic.eq ?A ==> ?R' => red ; intros ; subst ; red_subst_eq_morphism R'
+    | ?R ==> ?R' => red ; intros ; red_subst_eq_morphism R'
+    | _ => idtac
+  end.
+
+Ltac destruct_morphism :=
+  match goal with
+    | [ |- @Morphism ?A ?R ?m ] => constructor
+  end.
+
+Ltac reverse_arrows x :=
+  match x with
+    | @Logic.eq ?A ==> ?R' => revert_last ; reverse_arrows R'
+    | ?R ==> ?R' => do 3 revert_last ; reverse_arrows R'
+    | _ => idtac
+  end.
+
+Ltac add_morphism_tactic := (try destruct_morphism) ;
+  match goal with
+    | [ |- (?x ==> ?y) _ _ ] => red_subst_eq_morphism (x ==> y) ; reverse_arrows (x ==> y)
+  end.
   
 Lemma nequiv_equiv_trans : forall [ ! Equivalence A ] (x y z : A), x =/= y -> y === z -> x =/= z.
 Proof with auto.
diff --git a/theories/FSets/FMapFacts.v b/theories/FSets/FMapFacts.v
index 87111b1a75..78962fd1b6 100644
--- a/theories/FSets/FMapFacts.v
+++ b/theories/FSets/FMapFacts.v
@@ -660,48 +660,50 @@ Add Relation key E.eq
  transitivity proved by E.eq_trans 
  as KeySetoid.
 
-Add Relation t Equal 
- reflexivity proved by Equal_refl
- symmetry proved by Equal_sym
- transitivity proved by Equal_trans
+Implicit Arguments Equal [[elt]].
+
+Add Relation (t elt) Equal  
+ reflexivity proved by (@Equal_refl elt)
+ symmetry proved by (@Equal_sym elt)
+ transitivity proved by (@Equal_trans elt)
  as EqualSetoid.
 
-Add Morphism In with signature E.eq ==> Equal ==> iff as In_m.
+Add Morphism (@In elt) with signature E.eq ==> Equal ==> iff as In_m.
 Proof.
-unfold Equal; intros elt k k' Hk m m' Hm.
+unfold Equal; intros k k' Hk m m' Hm.
 rewrite (In_iff m Hk), in_find_iff, in_find_iff, Hm; intuition.
 Qed.
 
-Add Morphism MapsTo 
- with signature E.eq ==> @Logic.eq ==> Equal ==> iff as MapsTo_m.
+Add Morphism (@MapsTo elt)
+ with signature E.eq ==> Logic.eq ==> Equal ==> iff as MapsTo_m.
 Proof.
-unfold Equal; intros elt k k' Hk e m m' Hm.
+unfold Equal; intros k k' Hk e m m' Hm.
 rewrite (MapsTo_iff m e Hk), find_mapsto_iff, find_mapsto_iff, Hm; 
  intuition.
 Qed.
 
-Add Morphism Empty with signature Equal ==> iff as Empty_m.
+Add Morphism (@Empty elt) with signature Equal ==> iff as Empty_m.
 Proof.
-unfold Empty; intros elt m m' Hm; intuition.
+unfold Empty; intros m m' Hm; intuition.
 rewrite <-Hm in H0; eauto.
 rewrite Hm in H0; eauto.
 Qed.
 
-Add Morphism is_empty with signature Equal ==> @Logic.eq as is_empty_m.
+Add Morphism (@is_empty elt) with signature Equal ==> Logic.eq as is_empty_m.
 Proof.
-intros elt m m' Hm.
+intros m m' Hm.
 rewrite eq_bool_alt, <-is_empty_iff, <-is_empty_iff, Hm; intuition.
 Qed.
 
-Add Morphism mem with signature E.eq ==> Equal ==> @Logic.eq as mem_m.
+Add Morphism (@mem elt) with signature E.eq ==> Equal ==> Logic.eq as mem_m.
 Proof.
-intros elt k k' Hk m m' Hm.
+intros k k' Hk m m' Hm.
 rewrite eq_bool_alt, <- mem_in_iff, <-mem_in_iff, Hk, Hm; intuition.
 Qed.
 
-Add Morphism find with signature E.eq ==> Equal ==> @Logic.eq as find_m.
+Add Morphism (@find elt) with signature E.eq ==> Equal ==> Logic.eq as find_m.
 Proof.
-intros elt k k' Hk m m' Hm.
+intros k k' Hk m m' Hm.
 generalize (find_mapsto_iff m k)(find_mapsto_iff m' k')
  (not_find_in_iff m k)(not_find_in_iff m' k'); 
 do 2 destruct find; auto; intros.
@@ -710,27 +712,27 @@ rewrite <- H1, Hk, Hm, H2; auto.
 symmetry; rewrite <- H2, <-Hk, <-Hm, H1; auto.
 Qed.
 
-Add Morphism add with signature 
- E.eq ==> @Logic.eq ==> Equal ==> Equal as add_m.
+Add Morphism (@add elt) with signature 
+ E.eq ==> Logic.eq ==> Equal ==> Equal as add_m.
 Proof.
-intros elt k k' Hk e m m' Hm y.
+intros k k' Hk e m m' Hm y.
 rewrite add_o, add_o; do 2 destruct eq_dec; auto.
 elim n; rewrite <-Hk; auto.
 elim n; rewrite Hk; auto.
 Qed.
 
-Add Morphism remove with signature
+Add Morphism (@remove elt) with signature
  E.eq ==> Equal ==> Equal as remove_m.
 Proof.
-intros elt k k' Hk m m' Hm y.
+intros k k' Hk m m' Hm y.
 rewrite remove_o, remove_o; do 2 destruct eq_dec; auto.
 elim n; rewrite <-Hk; auto.
 elim n; rewrite Hk; auto.
 Qed.
 
-Add Morphism map with signature @Logic.eq ==> Equal ==> Equal as map_m.
+Add Morphism (@map elt elt') with signature Logic.eq ==> Equal ==> Equal as map_m.
 Proof.
-intros elt elt' f m m' Hm y.
+intros f m m' Hm y.
 rewrite map_o, map_o, Hm; auto.
 Qed.
 
@@ -1102,7 +1104,7 @@ Module WProperties (E:DecidableType)(M:WSfun E).
 
  End Elt.
 
- Add Morphism cardinal with signature Equal ==> @Logic.eq as cardinal_m.
+ Add Morphism (@cardinal elt) with signature Equal ==> Logic.eq as cardinal_m.
  Proof. intros; apply Equal_cardinal; auto. Qed.
 
 End WProperties.
diff --git a/theories/FSets/FSetFacts.v b/theories/FSets/FSetFacts.v
index 8ee74649e6..b0c8ee008c 100644
--- a/theories/FSets/FSetFacts.v
+++ b/theories/FSets/FSetFacts.v
@@ -339,7 +339,7 @@ exact (H1 (refl_equal true) _ Ha).
 Qed.
 
 Add Morphism Empty with signature Equal ==> iff as Empty_m.
-Proof. 
+Proof.
 intros; do 2 rewrite is_empty_iff; rewrite H; intuition.
 Qed.
 
@@ -429,13 +429,13 @@ Add Relation t Subset
    the two previous lemmas, in order to allow conversion of 
    SubsetSetoid coming from separate Facts modules. See bug #1738. *)
 
-Add Morphism In with signature E.eq ==> Subset ++> impl as In_s_m.
+Instance In_s_m : Morphism (E.eq ==> Subset ++> impl) In | 1.
 Proof.
-unfold Subset, impl; intros; eauto with set.
+  do 2 red ; intros. unfold Subset, impl; intros; eauto with set.
 Qed.
 
 Add Morphism Empty with signature Subset --> impl as Empty_s_m.
-Proof. 
+Proof.
 unfold Subset, Empty, impl; firstorder.
 Qed.
 
diff --git a/theories/FSets/FSetWeakList.v b/theories/FSets/FSetWeakList.v
index 866c3f6208..c2bba9283a 100644
--- a/theories/FSets/FSetWeakList.v
+++ b/theories/FSets/FSetWeakList.v
@@ -125,7 +125,7 @@ Module Raw (X: DecidableType).
   Lemma In_eq :
     forall (s : t) (x y : elt), X.eq x y -> In x s -> In y s.
   Proof.
-  intros s x y; do 2 setoid_rewrite InA_alt; firstorder eauto.
+  intros s x y; setoid_rewrite InA_alt; firstorder eauto.
   Qed.
   Hint Immediate In_eq.
 
diff --git a/theories/Numbers/Integer/TreeMod/ZTreeMod.v b/theories/Numbers/Integer/TreeMod/ZTreeMod.v
index db09c2ec7a..e885d25bc7 100644
--- a/theories/Numbers/Integer/TreeMod/ZTreeMod.v
+++ b/theories/Numbers/Integer/TreeMod/ZTreeMod.v
@@ -143,7 +143,7 @@ Hypothesis A0 : A 0.
 Hypothesis AS : forall n : NZ, A n <-> A (S n). (* Below, we use only -> direction *)
 
 Add Morphism A with signature NZeq ==> iff as A_morph.
-Proof A_wd.
+Proof. apply A_wd. Qed.
 
 Let B (n : Z) := A (Z_to_NZ n).
 
diff --git a/theories/Numbers/NatInt/NZBase.v b/theories/Numbers/NatInt/NZBase.v
index 730d8a00fd..084560de3b 100644
--- a/theories/Numbers/NatInt/NZBase.v
+++ b/theories/Numbers/NatInt/NZBase.v
@@ -64,7 +64,7 @@ something like this. The same goes for "relation". *)
 Hypothesis A_wd : predicate_wd NZeq A.
 
 Add Morphism A with signature NZeq ==> iff as A_morph.
-Proof A_wd.
+Proof. apply A_wd. Qed.
 
 Theorem NZcentral_induction :
   forall z : NZ, A z ->
diff --git a/theories/Numbers/NatInt/NZOrder.v b/theories/Numbers/NatInt/NZOrder.v
index 0708e060a2..bc3600f9ce 100644
--- a/theories/Numbers/NatInt/NZOrder.v
+++ b/theories/Numbers/NatInt/NZOrder.v
@@ -396,7 +396,7 @@ Variable A : NZ -> Prop.
 Hypothesis A_wd : predicate_wd NZeq A.
 
 Add Morphism A with signature NZeq ==> iff as A_morph.
-Proof A_wd.
+Proof. apply A_wd. Qed.
 
 Section Center.
 
diff --git a/theories/Numbers/Natural/Abstract/NBase.v b/theories/Numbers/Natural/Abstract/NBase.v
index 0a3d1a586e..27d9c72bdc 100644
--- a/theories/Numbers/Natural/Abstract/NBase.v
+++ b/theories/Numbers/Natural/Abstract/NBase.v
@@ -81,7 +81,7 @@ function (by recursion) that maps 0 to false and the successor to true *)
 Definition if_zero (A : Set) (a b : A) (n : N) : A :=
   recursion a (fun _ _ => b) n.
 
-Add Morphism if_zero with signature @eq ==> @eq ==> Neq ==> @eq as if_zero_wd.
+Add Morphism (if_zero A) with signature (eq ==> eq ==> Neq ==> eq) as if_zero_wd.
 Proof.
 intros; unfold if_zero. apply recursion_wd with (Aeq := (@eq A)).
 reflexivity. unfold fun2_eq; now intros. assumption.
diff --git a/theories/Numbers/Natural/Abstract/NOrder.v b/theories/Numbers/Natural/Abstract/NOrder.v
index 9ddaa9a2f0..7b4645be35 100644
--- a/theories/Numbers/Natural/Abstract/NOrder.v
+++ b/theories/Numbers/Natural/Abstract/NOrder.v
@@ -407,7 +407,7 @@ Variable R : N -> N -> Prop.
 Hypothesis R_wd : relation_wd Neq Neq R.
 
 Add Morphism R with signature Neq ==> Neq ==> iff as R_morph2.
-Proof R_wd.
+Proof. apply R_wd. Qed.
 
 Theorem le_ind_rel :
    (forall m : N, R 0 m) ->
diff --git a/theories/Numbers/NumPrelude.v b/theories/Numbers/NumPrelude.v
index e66bc8ebfc..c063c7bc1d 100644
--- a/theories/Numbers/NumPrelude.v
+++ b/theories/Numbers/NumPrelude.v
@@ -148,15 +148,15 @@ intros R1 R2 R3 H1 H2 x y; rewrite H1; apply H2.
 now symmetry.
 Qed.
 
-Add Relation (fun A B : Type => A -> B -> Prop) relations_eq
-  reflexivity proved by (fun A B : Type => proj1 (relations_eq_equiv A B))
-  symmetry proved by (fun A B : Type => proj2 (proj2 (relations_eq_equiv A B)))
-  transitivity proved by (fun A B : Type => proj1 (proj2 (relations_eq_equiv A B)))
+Add Relation (A -> B -> Prop) (@relations_eq A B)
+  reflexivity proved by (proj1 (relations_eq_equiv A B))
+  symmetry proved by (proj2 (proj2 (relations_eq_equiv A B)))
+  transitivity proved by (proj1 (proj2 (relations_eq_equiv A B)))
 as relations_eq_rel.
 
-Add Morphism well_founded with signature relations_eq ==> iff as well_founded_wd.
+Add Morphism (@well_founded A) with signature (@relations_eq A A) ==> iff as well_founded_wd.
 Proof.
-unfold relations_eq, well_founded; intros A R1 R2 H;
+unfold relations_eq, well_founded; intros R1 R2 H;
 split; intros H1 a; induction (H1 a) as [x H2 H3]; constructor;
 intros y H4; apply H3; [now apply <- H | now apply -> H].
 Qed.
diff --git a/theories/QArith/QArith_base.v b/theories/QArith/QArith_base.v
index 5199333ede..cde670075b 100644
--- a/theories/QArith/QArith_base.v
+++ b/theories/QArith/QArith_base.v
@@ -200,7 +200,7 @@ Proof.
   unfold Qeq, Qopp; simpl.
   Open Scope Z_scope.
   intros.
-  replace (- Qnum x1 * ' Qden x2) with (- (Qnum x1 * ' Qden x2)) by ring.
+  replace (- Qnum x * ' Qden y) with (- (Qnum x * ' Qden y)) by ring.
   rewrite H in |- *;  ring.
   Close Scope Z_scope.
 Qed.
diff --git a/theories/Relations/Relation_Operators.v b/theories/Relations/Relation_Operators.v
index 8d76b4f4e0..61b70ba689 100644
--- a/theories/Relations/Relation_Operators.v
+++ b/theories/Relations/Relation_Operators.v
@@ -83,9 +83,9 @@ Variable leA : A -> A -> Prop.
 Variable leB : B -> B -> Prop.
 
 Inductive le_AsB : A + B -> A + B -> Prop :=
-  | le_aa : forall x y:A, leA x y -> le_AsB (inl B x) (inl B y)
-  | le_ab : forall (x:A) (y:B), le_AsB (inl B x) (inr A y)
-  | le_bb : forall x y:B, leB x y -> le_AsB (inr A x) (inr A y).
+  | le_aa : forall x y:A, leA x y -> le_AsB (inl x) (inl y)
+  | le_ab : forall (x:A) (y:B), le_AsB (inl x) (inr y)
+  | le_bb : forall x y:B, leB x y -> le_AsB (inr x) (inr y).
 
 End Disjoint_Union. 
 
diff --git a/theories/Setoids/Setoid.v b/theories/Setoids/Setoid.v
index f93a12955c..34bff63547 100644
--- a/theories/Setoids/Setoid.v
+++ b/theories/Setoids/Setoid.v
@@ -10,8 +10,8 @@
 
 Set Implicit Arguments.
 
-Require Export Setoid_tac.
-Require Export Setoid_Prop.
+Require Export Coq.Classes.Equivalence.
+Require Export Coq.Relations.Relation_Definitions.
 
 (** For backward compatibility *)
 
diff --git a/theories/Sorting/Permutation.v b/theories/Sorting/Permutation.v
index 026a305b1c..2f8ef8d118 100644
--- a/theories/Sorting/Permutation.v
+++ b/theories/Sorting/Permutation.v
@@ -8,7 +8,7 @@
 
 (*i $Id$ i*)
 
-Require Import Relations.
+Require Import Coq.Relations.Relations.
 Require Import List.
 Require Import Multiset.
 Require Import Arith.
diff --git a/theories/Wellfounded/Disjoint_Union.v b/theories/Wellfounded/Disjoint_Union.v
index f6ce84f986..a86d19c09d 100644
--- a/theories/Wellfounded/Disjoint_Union.v
+++ b/theories/Wellfounded/Disjoint_Union.v
@@ -21,7 +21,7 @@ Section Wf_Disjoint_Union.
 
   Notation Le_AsB := (le_AsB A B leA leB).
   
-  Lemma acc_A_sum : forall x:A, Acc leA x -> Acc Le_AsB (inl B x).
+  Lemma acc_A_sum : forall x:A, Acc leA x -> Acc Le_AsB (inl x).
   Proof.
     induction 1.
     apply Acc_intro; intros y H2.
@@ -30,7 +30,7 @@ Section Wf_Disjoint_Union.
   Qed.
 
   Lemma acc_B_sum :
-    well_founded leA -> forall x:B, Acc leB x -> Acc Le_AsB (inr A x).
+    well_founded leA -> forall x:B, Acc leB x -> Acc Le_AsB (inr x).
   Proof.
     induction 2.
     apply Acc_intro; intros y H3.
diff --git a/theories/ZArith/Zdiv.v b/theories/ZArith/Zdiv.v
index de3b76e95d..ff8033eeb4 100644
--- a/theories/ZArith/Zdiv.v
+++ b/theories/ZArith/Zdiv.v
@@ -931,7 +931,7 @@ Module EqualityModulo (M:SomeNumber).
 
  Add Morphism Zopp : Zopp_eqm.
  Proof.
-  intros; change (-x1 == -x2) with (0-x1 == 0-x2).
+  intros; change (-x == -y) with (0-x == 0-y).
   rewrite H; red; auto.
  Qed.