New reflexive implementation of setoid_rewrite. The new implementation

introduces a few backward incompatibilities:
 1. setoid_replace used to try to close the new goal using full_trivial.
    The new implementation does not try to close the goal.
    To fix the script it is sufficient to add a "; [ idtac | trivial ]."
    after every application of setoid_replace that used to generate just
    one goal.
 2. (setoid_replace c1 c2) used to replace either c1 with c2 or c2 with c1
    (if c1 did not occur in the goal). The new implementation only replaces
    c1 with c2.
    To fix the script it is sufficient to replace
    (setoid_replace c1 with c2) with
    (setoid_replace c1 with c2) || (setoid_replace c2 with c1)
    in those cases where it is unknown what should be substituted with what.
 3. the goal generated by the "Add Morphism" command has the hypothesis
    permutated w.r.t. the old implementation. I.e. the old implementation
    used to generate: forall x1 x2, forall x3 x4, x1=x2 -> x3=x4 -> ...
    whereas the new implementation generates
     forall x1 x2, x1=x2 -> forall x3 x4, x3 = x4 -> ...
    Fixing the script is usually trivial.
 4. the "Add Morphism P" command used to generate a non-standard goal in the
    case of P being a predicate (i.e. a function whose codomain is Prop).
    In that case the goal ended with an implication (instead of ending with
    a coimplication). The new implementation generates a standard goal that
    ends with a coimplication.
    To fix the script you can add the following line at the very beginning:
     cut <<old_goal>>; intro Hold; split; apply Hold;
      assumption || (symmetry;assumption).


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

3 files changed, 941 insertions, 674 deletions

diff --git a/tactics/setoid_replace.ml b/tactics/setoid_replace.ml
index 4a44e72d2..a5f5f742d 100644
--- a/tactics/setoid_replace.ml
+++ b/tactics/setoid_replace.ml
@@ -33,21 +33,22 @@ open Constrintern
 let replace = ref (fun _ _ -> assert false)
 let register_replace f = replace := f
 
-type setoid =
-    { set_a : constr;
-      set_aeq : constr;
-      set_th : constr
-    }
-
-type 'a setoid_class =
-   ACSetoid  of 'a      (*the equivalence relation of the setoid or the setoid*)
- | ACLeibniz of constr  (*the carrier of the setoid*)
+type reflexive_relation =
+   { refl_a: constr ;
+     refl_aeq: constr;
+     refl_refl: constr;
+     refl_sym: constr option
+   }
+
+type 'a relation_class =
+   ACReflexive of 'a    (* the relation of the reflexive_relation
+                           or the reflexive_relation*)
+ | ACLeibniz of constr  (* the carrier *)
 
 type 'a morphism =
-    { lem : constr;
-      args : 'a setoid_class list;
-      output : 'a setoid_class;
-      lem2 : constr option
+    { args : 'a relation_class list;
+      output : 'a relation_class;
+      lem : constr;
     }
 
 type funct =
@@ -56,25 +57,27 @@ type funct =
     }
 
 type morphism_class =
-   ACMorphism of setoid morphism
+   ACMorphism of reflexive_relation morphism
  | ACFunction of funct
 
-let subst_mps_in_setoid_class subst =
+let subst_mps_in_relation_class subst =
  function
-    ACSetoid  t -> ACSetoid  (subst_mps subst t)
+    ACReflexive  t -> ACReflexive  (subst_mps subst t)
   | ACLeibniz t -> ACLeibniz (subst_mps subst t) 
 
-let constr_setoid_class_of_setoid_setoid_class =
+let constr_relation_class_of_relation_relation_class =
  function
-    ACSetoid setoid -> ACSetoid setoid.set_aeq
+    ACReflexive relation -> ACReflexive relation.refl_aeq
   | ACLeibniz t -> ACLeibniz t
  
 
 let constr_of c = Constrintern.interp_constr Evd.empty (Global.env()) c
 
 let constant dir s = Coqlib.gen_constant "Setoid_replace" ("Setoids"::dir) s
-
-let global_constant dir s =Coqlib.gen_constant "Setoid_replace" ("Init"::dir) s
+let init_constant dir s = Coqlib.gen_constant "Setoid_replace" ("Init"::dir) s
+let reference dir s = Coqlib.gen_reference "Setoid_replace" ("Setoids"::dir) s
+let eval_reference dir s = EvalConstRef (destConst (constant dir s))
+let eval_init_reference dir s = EvalConstRef (destConst (init_constant dir s))
 
 let current_constant id =
   try
@@ -82,134 +85,196 @@ let current_constant id =
   with Not_found ->
     anomaly ("Setoid: cannot find " ^ (string_of_id id))
 
-(* Setoid_theory *)
+(* From Setoid.v *)
 
+let coq_is_reflexive = lazy(constant ["Setoid"] "is_reflexive")
+
+let coq_Relation_Class = lazy(constant ["Setoid"] "Relation_Class")
 let coq_Setoid_Theory = lazy(constant ["Setoid"] "Setoid_Theory")
+let coq_Morphism_Theory = lazy(constant ["Setoid"] "Morphism_Theory")
+let coq_Build_Morphism_Theory= lazy(constant ["Setoid"] "Build_Morphism_Theory")
+
+let coq_Reflexive = lazy(constant ["Setoid"] "Reflexive")
+let coq_Leibniz = lazy(constant ["Setoid"] "Leibniz")
 
 let coq_seq_refl = lazy(constant ["Setoid"] "Seq_refl")
 let coq_seq_sym = lazy(constant ["Setoid"] "Seq_sym")
 let coq_seq_trans = lazy(constant ["Setoid"] "Seq_trans")
 
-let coq_fleche = lazy(constant ["Setoid"] "fleche")
+let coq_singl = lazy(constant ["Setoid"] "singl")
+let coq_cons = lazy(constant ["Setoid"] "cons")
 
-(* Coq constants *)
+let coq_equality_morphism_of_setoid_theory =
+ lazy(constant ["Setoid"] "equality_morphism_of_setoid_theory")
+let coq_make_compatibility_goal =
+ lazy(constant ["Setoid"] "make_compatibility_goal")
+let coq_make_compatibility_goal_ref =
+ lazy(reference ["Setoid"] "make_compatibility_goal")
+let coq_make_compatibility_goal_aux_ref =
+ lazy(reference ["Setoid"] "make_compatibility_goal_aux")
 
-let coqiff = lazy(global_constant ["Logic"] "iff")
+let coq_App = lazy(constant ["Setoid"] "App")
+let coq_Toreplace = lazy(constant ["Setoid"] "Toreplace")
+let coq_Tokeep = lazy(constant ["Setoid"] "Tokeep")
+let coq_Imp = lazy(constant ["Setoid"] "Imp")
+let coq_fcl_singl = lazy(constant ["Setoid"] "fcl_singl")
+let coq_fcl_cons = lazy(constant ["Setoid"] "fcl_cons")
 
-let coqeq = lazy(global_constant ["Logic"] "eq")
+let coq_setoid_rewrite = lazy(constant ["Setoid"] "setoid_rewrite")
+let coq_proj2 = lazy(init_constant ["Logic"] "proj2")
 
-let coqconj = lazy(global_constant ["Logic"] "conj")
-let coqand = lazy(global_constant ["Logic"] "and")
-let coqproj1 = lazy(global_constant ["Logic"] "proj1")
-let coqproj2 = lazy(global_constant ["Logic"] "proj2")
+let coq_morphism_theory_of_function =
+ lazy(constant ["Setoid"] "morphism_theory_of_function")
+let coq_morphism_theory_of_predicate =
+ lazy(constant ["Setoid"] "morphism_theory_of_predicate")
+let coq_relation_of_relation_class =
+ lazy(eval_reference ["Setoid"] "relation_of_relation_class")
+let coq_interp = lazy(eval_reference ["Setoid"] "interp")
+let coq_Morphism_Context_rect2 =
+ lazy(eval_reference ["Setoid"] "Morphism_Context_rect2")
+let coq_iff = lazy(eval_init_reference ["Logic"] "iff")
 
-(************************* Table of declared setoids **********************)
+let coq_prop_relation =
+ lazy (
+  ACReflexive {
+     refl_a = mkProp ;
+     refl_aeq = init_constant ["Logic"] "iff" ;
+     refl_refl = init_constant ["Logic"] "iff_refl";
+     refl_sym = Some (init_constant ["Logic"] "iff_sym")
+   })
 
 
-(* Setoids are stored in a table which is synchronised with the Reset mechanism. *)
+(************************* Table of declared relations **********************)
+
 
-let setoid_table = ref Gmap.empty
+(* Relations are stored in a table which is synchronised with the Reset mechanism. *)
 
-let setoid_table_add (s,th) = setoid_table := Gmap.add s th !setoid_table
-let setoid_table_find s = Gmap.find s !setoid_table
-let setoid_table_mem s = Gmap.mem s !setoid_table
+let relation_table = ref Gmap.empty
 
-let prsetoid s =
- str "(" ++ prterm s.set_a ++ str "," ++ prterm s.set_aeq ++ str ")"
+let relation_table_add (s,th) = relation_table := Gmap.add s th !relation_table
+let relation_table_find s = Gmap.find s !relation_table
+let relation_table_mem s = Gmap.mem s !relation_table
 
-let prsetoid_class =
+let prrelation s =
+ str "(" ++ prterm s.refl_a ++ str "," ++ prterm s.refl_aeq ++ str ")"
+
+let prrelation_class =
  function
-    ACSetoid eq  ->
-     (try prsetoid (setoid_table_find eq)
+    ACReflexive eq  ->
+     (try prrelation (relation_table_find eq)
       with Not_found ->
+       (*CSC: still "setoid" in the error message *)
        str "[[ Error: setoid on equality " ++ prterm eq ++ str " not found! ]]")
   | ACLeibniz ty -> prterm ty
 
 let prmorphism k m =
   prterm k ++ str ": " ++
-  prlist_with_sep (fun () -> str " -> ") prsetoid_class m.args ++
-  str " -> " ++ prsetoid_class m.output
+  prlist_with_sep (fun () -> str " -> ") prrelation_class m.args ++
+  str " -> " ++ prrelation_class m.output
 
 
-(* A function that gives back the only setoid on a given carrier *)
+(* A function that gives back the only relation_class on a given carrier *)
 (*CSC: this implementation is really inefficient. I should define a new
   map to make it efficient. However, is this really worth of? *)
-let default_setoid_for_carrier a =
- let rng = Gmap.rng !setoid_table in
- match List.filter (fun {set_a=set_a} -> set_a = a) rng with
+let default_relation_for_carrier a =
+ let rng = Gmap.rng !relation_table in
+ match List.filter (fun {refl_a=refl_a} -> refl_a = a) rng with
     [] -> ACLeibniz a
-  | setoid::tl ->
+  | relation::tl ->
      if tl <> [] then
       msg_warning
+       (*CSC: still "setoid" in the error message *)
        (str "There are several setoids whose carrier is " ++ prterm a ++
-         str ". The setoid " ++ prsetoid setoid ++
+         str ". The setoid " ++ prrelation relation ++
          str " is randomly chosen.") ;
-     ACSetoid setoid
+     ACReflexive relation
 
-let setoid_morphism_of_constr_morphism =
- let setoid_setoid_class_of_constr_setoid_class =
+let relation_morphism_of_constr_morphism =
+ let relation_relation_class_of_constr_relation_class =
   function
      ACLeibniz t -> ACLeibniz t
-   | ACSetoid aeq ->
-      ACSetoid (try setoid_table_find aeq with Not_found -> assert false)
+   | ACReflexive aeq ->
+      ACReflexive (try relation_table_find aeq with Not_found -> assert false)
  in
   function mor ->
-   let args' = List.map setoid_setoid_class_of_constr_setoid_class mor.args in
-   let output' = setoid_setoid_class_of_constr_setoid_class mor.output in
+   let args' = List.map relation_relation_class_of_constr_relation_class mor.args in
+   let output' = relation_relation_class_of_constr_relation_class mor.output in
     {mor with args=args' ; output=output'}
 
-let subst_setoid subst setoid = 
-  let set_a' = subst_mps subst setoid.set_a in
-  let set_aeq' = subst_mps subst setoid.set_aeq in
-  let set_th' = subst_mps subst setoid.set_th in
-    if set_a' == setoid.set_a
-      && set_aeq' == setoid.set_aeq
-      && set_th' == setoid.set_th
+let subst_relation subst relation = 
+  let refl_a' = subst_mps subst relation.refl_a in
+  let refl_aeq' = subst_mps subst relation.refl_aeq in
+  let refl_refl' = subst_mps subst relation.refl_refl in
+  let refl_sym' = option_app (subst_mps subst) relation.refl_sym in
+    if refl_a' == relation.refl_a
+      && refl_aeq' == relation.refl_aeq
+      && refl_refl' == relation.refl_refl
+      && refl_sym' == relation.refl_sym
     then
-      setoid
+      relation
     else
-      { set_a = set_a' ;
-	set_aeq = set_aeq' ;
-	set_th = set_th' ;
+      { refl_a = refl_a' ;
+        refl_aeq = refl_aeq' ;
+        refl_refl = refl_refl' ;
+        refl_sym = refl_sym'
       }
       
-let equiv_list () = List.map (fun x -> x.set_aeq) (Gmap.rng !setoid_table)
+let equiv_list () = List.map (fun x -> x.refl_aeq) (Gmap.rng !relation_table)
 
 let _ = 
-  Summary.declare_summary "setoid-table"
-    { Summary.freeze_function = (fun () -> !setoid_table);
-      Summary.unfreeze_function = (fun t -> setoid_table := t);
-      Summary.init_function = (fun () -> setoid_table := Gmap .empty);
+  Summary.declare_summary "relation-table"
+    { Summary.freeze_function = (fun () -> !relation_table);
+      Summary.unfreeze_function = (fun t -> relation_table := t);
+      Summary.init_function = (fun () -> relation_table := Gmap .empty);
       Summary.survive_module = true;
       Summary.survive_section = false }
 
-(* Declare a new type of object in the environment : "setoid-theory". *)
+(* Declare a new type of object in the environment : "relation-theory". *)
 
-let (setoid_to_obj, obj_to_setoid)=
+let (relation_to_obj, obj_to_relation)=
   let cache_set (_,(s, th)) =
-   if setoid_table_mem s then
-    begin
-     let old_setoid = setoid_table_find s in
-      msg_warning
-       (str "The setoid " ++ prsetoid th ++ str " is redeclared. " ++
-        str "The new declaration justified by " ++
-         prterm th.set_th ++ str " replaces the old declaration justified by "++
-         prterm old_setoid.set_th ++ str ".")
-    end ;
-   setoid_table_add (s,th)
+   let th' =
+    if relation_table_mem s then
+     begin
+      let old_relation = relation_table_find s in
+       let th' =
+        {th with refl_sym =
+          match th.refl_sym with
+             None -> old_relation.refl_sym
+           | Some t -> Some t} in
+        (*CSC: still "setoid" in the error message *)
+        msg_warning
+         (str "The setoid " ++ prrelation th' ++ str " is redeclared. " ++
+          str "The new declaration (reflevity proved by " ++
+           prterm th'.refl_refl ++
+           (match th'.refl_sym with
+               None -> str ""
+             | Some t -> str " and symmetry proved by " ++ prterm t) ++
+           str ") replaces the old declaration (reflexivity proved by "++
+           prterm old_relation.refl_refl ++
+           (match old_relation.refl_sym with
+               None -> str ""
+             | Some t -> str " and symmetry proved by " ++ prterm t) ++
+           str ").") ;
+        th'
+     end
+    else
+     th
+   in
+    relation_table_add (s,th')
   and subst_set (_,subst,(s,th as obj)) =
     let s' = subst_mps subst s in
-    let th' = subst_setoid subst th in
+    let th' = subst_relation subst th in
       if s' == s && th' == th then obj else
-	(s',th')
+        (s',th')
   and export_set x = Some x 
   in 
-    declare_object {(default_object "setoid-theory") with
-		      cache_function = cache_set;
-		      load_function = (fun i o -> cache_set o);
-		      subst_function = subst_set;
-		      classify_function = (fun (_,x) -> Substitute x);
-		      export_function = export_set}
+    declare_object {(default_object "relation-theory") with
+                      cache_function = cache_set;
+                      load_function = (fun i o -> cache_set o);
+                      subst_function = subst_set;
+                      classify_function = (fun (_,x) -> Substitute x);
+                      export_function = export_set}
 
 (******************************* Table of declared morphisms ********************)
 
@@ -233,47 +298,25 @@ let morphism_table_add (m,c) =
     msg_warning
      (str "The morphism " ++ prmorphism m old_morph ++ str " is redeclared. " ++
       str "The new declaration whose compatibility is granted by " ++
-       prterm c.lem ++
-       (match c.lem2 with None -> str "" | Some t-> str " and " ++ prterm t)
-       ++ str " replaces the old declaration whose" ++
+       prterm c.lem ++ str " replaces the old declaration whose" ++
        str " compatibility was granted by " ++
-       prterm old_morph.lem ++
-       (match old_morph.lem2 with
-          None -> str ""
-        | Some t-> str " and "++ prterm t) ++ str ".")
+       prterm old_morph.lem ++ str ".")
   with
    Not_found -> morphism_table := Gmap.add m (c::old) !morphism_table
 
-let find_morphism_fleche () =
- let fleche_constr = (Lazy.force coq_fleche) in
- try
-  let mor =
-   List.find
-    (function {args=args; output=output} as morphism ->
-      output = ACSetoid (Lazy.force coqiff) &&
-      List.for_all (function c -> c = ACSetoid (Lazy.force coqiff)) args)
-     (morphism_table_find fleche_constr)
-  in
-   setoid_morphism_of_constr_morphism mor
- with
-  Not_found -> assert false
-
 let subst_morph subst morph = 
   let lem' = subst_mps subst morph.lem in
-  let args' = list_smartmap (subst_mps_in_setoid_class subst) morph.args in
-  let output' = subst_mps_in_setoid_class subst morph.output in
-  let lem2' = option_smartmap (subst_mps subst) morph.lem2 in
+  let args' = list_smartmap (subst_mps_in_relation_class subst) morph.args in
+  let output' = subst_mps_in_relation_class subst morph.output in
     if lem' == morph.lem
       && args' == morph.args
       && output' == morph.output
-      && lem2' == morph.lem2
     then
       morph
     else
-      { lem = lem' ;
-	args = args' ;
-	output = output' ;
-	lem2 = lem2'
+      { args = args' ;
+        output = output' ;
+        lem = lem'
       }
 
 
@@ -293,144 +336,65 @@ let (morphism_to_obj, obj_to_morphism)=
     let m' = subst_mps subst m in
     let c' = subst_morph subst c in
       if m' == m && c' == c then obj else
-	(m',c')
+        (m',c')
   and export_set x = Some x 
   in 
     declare_object {(default_object "morphism-definition") with
-		      cache_function = cache_set;
-		      load_function = (fun i o -> cache_set o);
-		      subst_function = subst_set;
-		      classify_function = (fun (_,x) -> Substitute x);
-		      export_function = export_set}
+                      cache_function = cache_set;
+                      load_function = (fun i o -> cache_set o);
+                      subst_function = subst_set;
+                      classify_function = (fun (_,x) -> Substitute x);
+                      export_function = export_set}
 
-(************************** Printing setoids and morphisms **********************)
+(************************** Printing relations and morphisms **********************)
 
+(*CSC: still "setoids" in the name *)
 let print_setoids () =
   Gmap.iter
-   (fun k setoid ->
-     assert (k=setoid.set_aeq) ;
-     ppnl (str"Setoid " ++ prsetoid setoid ++ str"; equivalence relation properties granted by " ++
-      prterm setoid.set_th))
-   !setoid_table ;
+   (fun k relation ->
+     assert (k=relation.refl_aeq) ;
+     (*CSC: still "Setoid" in the error message *)
+     ppnl (str"Setoid " ++ prrelation relation ++
+      str"; reflexivity granted by " ++ prterm relation.refl_refl ++
+      (match relation.refl_sym with
+          None -> str ""
+        | Some t -> str " symmetry granted by " ++ prterm t)))
+   !relation_table ;
   Gmap.iter
    (fun k l ->
      List.iter
-      (fun ({lem=lem ; lem2=lem2} as mor) ->
+      (fun ({lem=lem} as mor) ->
         ppnl (str "Morphism " ++ prmorphism k mor ++
         str ". Compatibility granted by " ++
-        prterm lem ++ 
-         (match lem2 with None -> str"" | Some t -> str " and " ++ prterm t) ++
-        str "."))
+        prterm lem ++ str "."))
       l) !morphism_table
 ;;
 
-(************************** Adding a setoid to the database *********************)
-
-(* Add a Setoid to the database after a type verification. *)
-
-let eq_lem_common_sign env a eq =
-  let na = named_hd env a Anonymous in
-  let ne = named_hd env eq Anonymous in
-  [(ne,None,mkApp (eq, [|(mkRel 3);(mkRel 2)|]));
-   (ne,None,mkApp (eq, [|(mkRel 4);(mkRel 3)|]));
-   (na,None,a);(na,None,a);(na,None,a);(na,None,a)]
-
-(* Proof of (a,b,c,d:A)(eq a b)->(eq c d)->(eq a c)->(eq b d) *)
-let eq_lem_proof env a eq sym trans = 
-  let sign = eq_lem_common_sign env a eq in
-  let ne = named_hd env eq Anonymous in
-  let sign = (ne,None,mkApp (eq, [|(mkRel 6);(mkRel 4)|]))::sign in
-  let ccl = mkApp (eq, [|(mkRel 6);(mkRel 4)|]) in
-  let body =
-    mkApp (trans,
-      [|(mkRel 6);(mkRel 7);(mkRel 4);
-        (mkApp (sym, [|(mkRel 7);(mkRel 6);(mkRel 3)|]));
-	  (mkApp (trans,
-	    [|(mkRel 7);(mkRel 5);(mkRel 4);(mkRel 1);(mkRel 2)|]))|]) in
-  let p = it_mkLambda_or_LetIn body sign in
-  let t = it_mkProd_or_LetIn ccl sign in
-  (p,t)
-
-(* Proof of (a,b,c,d:A)(eq a b)->(eq c d)->((eq a c)<->(eq b d)) *)
-let eq_lem2_proof env a eq sym trans =
-  let sign = eq_lem_common_sign env a eq in
-  let ccl1 =
-    mkArrow
-      (mkApp (eq, [|(mkRel 6);(mkRel 4)|]))
-      (mkApp (eq, [|(mkRel 6);(mkRel 4)|])) in
-  let ccl2 =
-    mkArrow
-      (mkApp (eq, [|(mkRel 5);(mkRel 3)|]))
-      (mkApp (eq, [|(mkRel 7);(mkRel 5)|])) in
-  let ccl = mkApp (Lazy.force coqand, [|ccl1;ccl2|]) in
-  let body =
-    mkApp ((Lazy.force coqconj),
-    [|ccl1;ccl2;
-      lambda_create env
-	(mkApp (eq, [|(mkRel 6);(mkRel 4)|]),
-	(mkApp (trans,
-	  [|(mkRel 6);(mkRel 7);(mkRel 4);
-	    (mkApp (sym, [|(mkRel 7);(mkRel 6);(mkRel 3)|]));
-	    (mkApp (trans,
-	      [|(mkRel 7);(mkRel 5);(mkRel 4);(mkRel 1);(mkRel 2)|]))|])));
-      lambda_create env
-        (mkApp (eq, [|(mkRel 5);(mkRel 3)|]),
-        (mkApp (trans,
-          [|(mkRel 7);(mkRel 6);(mkRel 5);(mkRel 3);
-            (mkApp (trans,
-              [|(mkRel 6);(mkRel 4);(mkRel 5);(mkRel 1);
-                (mkApp (sym, [|(mkRel 5);(mkRel 4);(mkRel 2)|]))|]))|])))|])
-  in
-  let p = it_mkLambda_or_LetIn body sign in
-  let t = it_mkProd_or_LetIn ccl sign in
-  (p,t)
-
-let gen_eq_lem_name =
-  let i = ref 0 in
-    function () -> 
-      incr i;
-      make_ident "setoid_eq_ext" (Some !i)
-
-let add_setoid a aeq th =
-  let env = Global.env () in
-    if (is_conv env Evd.empty (Typing.type_of env Evd.empty th)
-	  (mkApp ((Lazy.force coq_Setoid_Theory), [| a; aeq |])))
-    then (Lib.add_anonymous_leaf 
-	    (setoid_to_obj 
-	       (aeq, { set_a = a;
-		     set_aeq = aeq;
-		     set_th = th}));
-	  let sym = mkApp ((Lazy.force coq_seq_sym), [|a; aeq; th|]) in
-	  let trans = mkApp ((Lazy.force coq_seq_trans), [|a; aeq; th|]) in
-	  let (eq_morph, eq_morph_typ) = eq_lem_proof env a aeq sym trans in
-	  let (eq_morph2, eq_morph2_typ) = eq_lem2_proof env a aeq sym trans in
-	    Options.if_verbose ppnl (prterm a ++str " is registered as a setoid");
-	    let eq_ext_name = gen_eq_lem_name () in 
-	    let eq_ext_name2 = gen_eq_lem_name () in 
-	    let _ = Declare.declare_constant eq_ext_name
-		      ((DefinitionEntry {const_entry_body = eq_morph; 
-		                       const_entry_type = Some eq_morph_typ;
-                                       const_entry_opaque = true}),
-		       IsProof Lemma) in
-	    let _ = Declare.declare_constant eq_ext_name2
-		      ((DefinitionEntry {const_entry_body = eq_morph2; 
-				       const_entry_type = Some eq_morph2_typ;
-                                       const_entry_opaque = true}),
-		       IsProof Lemma) in
-	    let eqmorph = (current_constant eq_ext_name) in
-	    let eqmorph2 = (current_constant eq_ext_name2) in
-	      (Lib.add_anonymous_leaf
-		 (morphism_to_obj (aeq,
-				   { lem = eqmorph;
-                                     args = [ACSetoid aeq; ACSetoid aeq];
-                                     output = ACSetoid (Lazy.force coqiff);
-				     lem2 = (Some eqmorph2)})));
-	      Options.if_verbose ppnl (prterm aeq ++str " is registered as a morphism"))
-    else errorlabstrm "Add Setoid" (str "Not a valid setoid theory")
-
-(* The vernac command "Add Setoid" *)
-let add_setoid a aeq th =
-  add_setoid (constr_of a) (constr_of aeq) (constr_of th)
+(************************** Adding a relation to the database *********************)
+
+let int_add_relation a aeq refl sym =
+ match refl with
+    None -> assert false (*CSC: unimplemented yet*)
+  | Some refl ->
+     let env = Global.env () in
+       if
+        (is_conv env Evd.empty (Typing.type_of env Evd.empty refl)
+         (mkApp ((Lazy.force coq_is_reflexive), [| a; aeq |])))
+       then
+        Lib.add_anonymous_leaf 
+         (relation_to_obj 
+          (aeq, { refl_a = a;
+                  refl_aeq = aeq;
+                  refl_refl = refl;
+                  refl_sym = sym}))
+        else
+         errorlabstrm "Add Relation Class"
+          (str "Not a valid proof of reflexivity")
+
+(* The vernac command "Add Relation ..." *)
+let add_relation a aeq refl sym =
+ int_add_relation (constr_of a) (constr_of aeq) (option_app constr_of refl)
+  (option_app constr_of sym)
 
 (***************** Adding a morphism to the database ****************************)
 
@@ -458,64 +422,33 @@ let check_is_dependent t n =
     else false
   in aux t 0 n
 
-let gen_lem_name m = match kind_of_term m with 
-  | Var id -> add_suffix id "_ext"
-  | Const kn -> add_suffix (id_of_label (label kn)) "_ext"
-  | Ind (kn, i) -> add_suffix (id_of_label (label kn)) ((string_of_int i)^"_ext")
-  | Construct ((kn,i),j) -> add_suffix
-      (id_of_label (label kn)) ((string_of_int i)^(string_of_int j)^"_ext")
-  | _ -> errorlabstrm "New Morphism" (str "The term " ++ prterm m ++ str "is not a known name")
-
-let gen_lemma_tail m args body n =
-  let l = (List.length args) in
-  let a1 = Array.create l (mkRel 0) in
-  let a2 = Array.create l (mkRel 0) in
-  let rec aux i n = function
-    | (ACSetoid _)::tl -> 
-	a1.(i) <- (mkRel n);
-	a2.(i) <- (mkRel (n-1));
-	aux (i+1) (n-2) tl
-    | (ACLeibniz _)::tl ->
-	a1.(i) <- (mkRel n);
-	a2.(i) <- (mkRel n);
-	aux (i+1) (n-1) tl
-    | [] -> () in 
-    aux 0 n args;
-    if (match body with ACSetoid setoid when setoid.set_aeq = Lazy.force coqiff -> true | _ -> false)
-    then mkArrow (mkApp (m,a1)) (lift 1 (mkApp (m, a2)))
-    else
-     match body with
-        ACSetoid setoid ->
-         mkApp (setoid.set_aeq, [|(mkApp (m, a1)); (mkApp (m, a2))|])
-      | ACLeibniz t ->
-         mkApp ((Lazy.force coqeq), [|t; (mkApp (m, a1)); (mkApp (m, a2))|])
-
-let gen_lemma_middle m args body n =
-  let rec aux i n =
-   function
-    | [] -> gen_lemma_tail m args body n
-    | (ACSetoid setoid)::tl ->
-        let t = setoid.set_a in
-	mkArrow (mkApp (setoid.set_aeq, 
-			[|(mkRel i); (mkRel (i-1))|])) (aux (i-1) (n+1) tl)
-    | (ACLeibniz t)::tl -> aux (i-1) n tl
-  in aux n n args
-
-let gen_compat_lemma env m body args = 
-  let rec aux n =
-   function
-      (ACSetoid setoid)::tl ->
-        let t = setoid.set_a in
-	 prod_create env (t,(prod_create env (t, (aux (n+2) tl))))
-    | (ACLeibniz t)::tl ->
-	prod_create env (t, (aux (n+1) tl))
-    | [] -> gen_lemma_middle m args body n
-  in aux 0 args
+(*CSC: I do not like this very much. I would prefer relation classes
+  to be CIC objects. Keeping backward compatibility, however, is annoying. *)
+let cic_relation_class_of_relation_class =
+ function
+    ACReflexive {refl_a = refl_a; refl_aeq = refl_aeq; refl_refl = refl_refl} ->
+     mkApp ((Lazy.force coq_Reflexive), [| refl_a ; refl_aeq; refl_refl |])
+  | ACLeibniz t -> mkApp ((Lazy.force coq_Leibniz), [| t |])
+
+let gen_compat_lemma_statement output args m =
+ let rec mk_signature =
+  function
+     [] -> assert false
+   | [last] ->
+      mkApp ((Lazy.force coq_singl), [| Lazy.force coq_Relation_Class; last |])
+   | he::tl ->
+      mkApp ((Lazy.force coq_cons),
+       [| Lazy.force coq_Relation_Class; he ; mk_signature tl |])
+ in
+  let output = cic_relation_class_of_relation_class output in
+  let args= mk_signature (List.map cic_relation_class_of_relation_class args) in
+   args, output,
+    mkApp ((Lazy.force coq_make_compatibility_goal), [| args ; output ; m |])
 
 let new_morphism m id hook =
   let env = Global.env() in
   let typeofm = (Typing.type_of env Evd.empty m) in
-  let typ = (nf_betaiota typeofm) in  (* nf_bdi avant, mais bug *)
+  let typ = (nf_betaiota typeofm) in
   let (argsrev, output) = (decompose_prod typ) in
   let args_ty = (List.map snd (List.rev argsrev)) in
     if (args_ty=[])
@@ -524,371 +457,420 @@ let new_morphism m id hook =
     else if (check_is_dependent typ (List.length args_ty))
     then  errorlabstrm "New Morphism"
      (str "The term " ++ prterm m ++ str" should not be a dependent product")
-    else (
-     let args = List.map default_setoid_for_carrier args_ty in
-     let output = default_setoid_for_carrier output in
-     let lem = (gen_compat_lemma env m output args) in
-      new_edited id (m,args,output);
-      Pfedit.start_proof id (IsGlobal (Proof Lemma)) 
-       (Declare.clear_proofs (Global.named_context ()))
-       lem hook;
-      (Options.if_verbose msg (Pfedit.pr_open_subgoals ())))
-
-let rec sub_bool n = function
-  | [] -> []
-  | (ACSetoid setoid)::tl -> (setoid, n)::(sub_bool (n-2) tl)
-  | (ACLeibniz _)::tl -> (sub_bool (n-1) tl)
-
-let gen_lemma_iff_tail m mext args n k =
-  let a1 = Array.create k (mkRel 0) in
-  let a2 = Array.create k (mkRel 0) in
-  let nb = List.length args in
-  let b1 = Array.create nb (mkRel 0) in
-  let b2 = Array.create nb (mkRel 0) in
-  let rec aux i j = function
-    |[] -> ()
-    |(ACSetoid _)::tl ->
-       (a1.(i) <- (mkRel j);
-	a1.(i+1) <- (mkRel (j-1));
-	a2.(i) <- (mkRel (j-1));
-	a2.(i+1) <- (mkRel j);
-	aux (i+2) (j-2) tl)
-    |(ACLeibniz _)::tl ->
-       (a1.(i) <- (mkRel j);
-	a2.(i) <- (mkRel j);
-	aux (i+1) (j-1) tl) in
-  let rec aux2 i j = function
-    | ({set_a=a; set_th=th; set_aeq=aeq},p)::tl -> 
-	a1.(i) <- (mkRel j);
-	a2.(i) <- mkApp ((Lazy.force coq_seq_sym),
-		   [|a; aeq; th; (mkRel p); (mkRel (p-1)); (mkRel j)|]);
-	aux2 (i+1) (j-1) tl
-    | [] -> () in
-  let rec aux3 i j = function
-    | (ACSetoid _)::tl -> 
-	b1.(i) <- (mkRel j);
-	b2.(i) <- (mkRel (j-1));
-	aux3 (i+1) (j-2) tl
-    | (ACLeibniz _)::tl ->
-	b1.(i) <- (mkRel j);
-	b2.(i) <- (mkRel j);
-	aux3 (i+1) (j-1) tl
-    | [] -> () in 
-    aux 0 k args;
-    aux2 n (k-n) (sub_bool k args);
-    aux3 0 k args;
-    mkApp ((Lazy.force coqconj),
-	   [|(mkArrow (mkApp (m,b1)) (lift 1 (mkApp (m, b2))));
-	     (mkArrow (mkApp (m,b2)) (lift 1 (mkApp (m, b1))));
-	     (mkApp (mext, a1));(mkApp (mext, a2))|])
-
-let gen_lemma_iff_middle env m mext args n =
-  let rec aux i k =
-   function
-      [] -> gen_lemma_iff_tail m mext args n k
-    | (ACSetoid setoid)::tl ->
-	lambda_create env
-         ((mkApp (setoid.set_aeq, [|(mkRel i); (mkRel (i-1))|])),
-          (aux (i-1) (k+1) tl))
-    | (ACLeibniz t)::tl -> aux (i-1) k tl
-  in aux n n args
-
-let gen_lem_iff env m mext args =
-  let rec aux n =
-   function
-      (ACSetoid setoid)::tl ->
-        let t = setoid.set_a in
-	lambda_create env (t,(lambda_create env (t, (aux (n+2) tl))))
-    | (ACLeibniz t)::tl ->
-	lambda_create env (t, (aux (n+1) tl))
-    | [] -> gen_lemma_iff_middle env m mext args n
-  in aux 0 args
-
-let add_morphism lem_name (m,args,output) =
- let env = Global.env() in
- let mext = (current_constant lem_name) in
- let args_constr= List.map constr_setoid_class_of_setoid_setoid_class args in
- let output_constr = constr_setoid_class_of_setoid_setoid_class output in
-   (if (match output with ACSetoid setoid when setoid.set_aeq = Lazy.force coqiff -> true | _ -> false)
-    then
-     (let lem_2 = gen_lem_iff env m mext args in
-      let lem2_name = add_suffix lem_name "2" in
-      let _ = Declare.declare_constant lem2_name
-	    ((DefinitionEntry {const_entry_body = lem_2; 
-			     const_entry_type = None;
-                                    const_entry_opaque = true}),
-	     IsProof Lemma) in
-      let lem2 = (current_constant lem2_name) in
-	    (Lib.add_anonymous_leaf
-	       (morphism_to_obj (m, 
-				 { lem = mext;
-                                   args = args_constr;
-                                   output = output_constr;
-				   lem2 = (Some lem2)})));
-	    Options.if_verbose message ((string_of_id lem2_name) ^ " is defined"))
     else
-     (Lib.add_anonymous_leaf
-      (morphism_to_obj (m, 
-        { lem = mext;
-          args = args_constr;
-          output = output_constr;
-	  lem2 = None}))));
-      Options.if_verbose ppnl (prterm m ++str " is registered as a morphism")   
+     begin
+      let args = List.map default_relation_for_carrier args_ty in
+      let output = default_relation_for_carrier output in
+      let argsconstr,outputconstr,lem =
+       gen_compat_lemma_statement output args m
+      in
+       new_edited id (m,args,argsconstr,output,outputconstr);
+       Pfedit.start_proof id (IsGlobal (Proof Lemma)) 
+        (Declare.clear_proofs (Global.named_context ()))
+        lem hook;
+       (* "unfold make_compatibility_goal" *)
+       Pfedit.by
+        (Tactics.unfold_constr
+         (Lazy.force coq_make_compatibility_goal_ref)) ;
+       (* "unfold make_compatibility_goal_aux" *)
+       Pfedit.by
+        (Tactics.unfold_constr
+         (Lazy.force coq_make_compatibility_goal_aux_ref)) ;
+       (* "simpl" *)
+       Pfedit.by Tactics.simpl_in_concl ;
+       Options.if_verbose msg (Pfedit.pr_open_subgoals ());
+     end
+
+let add_morphism lemma_infos mor_name (m,args,output) =
+ let env = Global.env() in
+ begin
+  match lemma_infos with
+     None -> () (* the Morphism_Theory object has alrady been created *)
+   | Some (lem_name,argsconstr,outputconstr) ->
+      (* only the compatibility has been proved; we need to declare the
+         Morphism_Theory object *)
+     let mext = current_constant lem_name in
+     ignore (
+      Declare.declare_constant mor_name
+       (DefinitionEntry
+         {const_entry_body =
+           mkApp ((Lazy.force coq_Build_Morphism_Theory),
+            [| argsconstr; outputconstr; m ; mext |]);
+          const_entry_type = None;
+          const_entry_opaque = false},
+           IsDefinition))
+  end ;
+  let mmor = current_constant mor_name in
+  let args_constr =
+   List.map constr_relation_class_of_relation_relation_class args in
+  let output_constr = constr_relation_class_of_relation_relation_class output in
+   Lib.add_anonymous_leaf
+    (morphism_to_obj (m, 
+      { args = args_constr;
+        output = output_constr;
+        lem = mmor }));
+   Options.if_verbose ppnl (prterm m ++ str " is registered as a morphism")   
 
 let morphism_hook stre ref =
   let pf_id = id_of_global ref in
+  let mor_id = id_of_string (string_of_id pf_id ^ "_morphism_theory") in
+  let (m,args,argsconstr,output,outputconstr) = what_edited pf_id in
   if (is_edited pf_id)
   then 
-    (add_morphism pf_id (what_edited pf_id); no_more_edited pf_id)
+    add_morphism (Some (pf_id,argsconstr,outputconstr)) mor_id
+     (m,args,output); no_more_edited pf_id
 
 let new_named_morphism id m = new_morphism (constr_of m) id morphism_hook
 
+(************************ Add Setoid ******************************************)
+
+(*CSC: I do not like this. I would prefer more self-describing constant names *)
+let gen_morphism_name =
+  let i = ref 0 in
+    function () -> 
+      incr i;
+      make_ident "morphism_of_setoid_equality" (Some !i)
+
+(* The vernac command "Add Setoid" *)
+let add_setoid a aeq th =
+ let a = constr_of a in
+ let aeq = constr_of aeq in
+ let th = constr_of th in
+ let env = Global.env () in
+  if is_conv env Evd.empty (Typing.type_of env Evd.empty th)
+    (mkApp ((Lazy.force coq_Setoid_Theory), [| a; aeq |]))
+  then
+   begin
+    let refl = mkApp ((Lazy.force coq_seq_refl), [| a; aeq; th |]) in
+    let sym = mkApp ((Lazy.force coq_seq_sym), [| a; aeq; th |]) in
+    int_add_relation a aeq (Some refl) (Some sym) ;
+    let mor_name = gen_morphism_name () in
+    let _ =
+     Declare.declare_constant mor_name
+      (DefinitionEntry
+        {const_entry_body =
+          mkApp
+           ((Lazy.force coq_equality_morphism_of_setoid_theory),
+            [| a; aeq; th |]) ;
+         const_entry_type = None;
+         const_entry_opaque = false},
+        IsDefinition) in
+    let aeq_rel =
+     ACReflexive
+      {refl_a = a ; refl_aeq = aeq ; refl_refl = refl ; refl_sym = (Some sym)}
+    in
+     add_morphism None mor_name
+      (aeq,[aeq_rel;aeq_rel],Lazy.force coq_prop_relation)
+   end
+  else
+   errorlabstrm "Add Setoid" (str "Not a valid setoid theory")
+
+
 (****************************** The tactic itself *******************************)
 
 type constr_with_marks =
-  | MApp of morphism_class Lazy.t * constr_with_marks array 
-  | Toreplace of setoid
-  | Tokeep
+  | MApp of constr * morphism_class * constr_with_marks array 
+  | Toreplace
+  | Tokeep of constr
   | Mimp of constr_with_marks * constr_with_marks
 
 let is_to_replace = function
- | Tokeep -> false
- | Toreplace _ -> true
+ | Tokeep _ -> false
+ | Toreplace -> true
  | MApp _ -> true
  | Mimp _ -> true
 
 let get_mark a = 
   Array.fold_left (||) false (Array.map is_to_replace a)
 
-exception Use_replace
+type argument =
+   Toapply of constr         (* apply the function to the argument *)
+ | Toexpand of name * types  (* beta-expand the function w.r.t. an argument
+                                of this type *)
+let beta_expand c args_rev =
+ let rec to_expand =
+  function
+     [] -> []
+   | (Toapply _)::tl -> to_expand tl
+   | (Toexpand (name,s))::tl -> (name,s)::(to_expand tl) in
+ let rec aux n =
+  function
+     [] -> []
+   | (Toapply arg)::tl -> arg::(aux n tl)
+   | (Toexpand _)::tl -> (mkRel n)::(aux (n + 1) tl)
+ in
+  compose_lam (to_expand args_rev)
+   (mkApp (c, Array.of_list (List.rev (aux 1 args_rev))))
 
-let mark_occur gl hyp =
+let relation_of_hypothesis_and_term_to_rewrite gl (_,h) t =
+ let hypt = pf_type_of gl h in
+ let (heq, hargs) = decompose_app hypt in
+ let rec get_all_but_last_two =
+  function
+     []
+   | [_] -> assert false
+   | [_;_] -> []
+   | he::tl -> he::(get_all_but_last_two tl) in
+ let aeq = mkApp (heq,(Array.of_list (get_all_but_last_two hargs))) in
+  try
+   relation_table_find aeq
+  with Not_found ->
+   (*CSC: still "setoid" in the error message *)
+   errorlabstrm "Setoid_rewrite"
+    (prterm aeq ++ str " is not a setoid equality.")
+
+let mark_occur t in_c =
  let rec aux t in_c =
-  if (eq_constr t in_c) then
-   let sa =
-    match hyp with
-       None ->
-        (match default_setoid_for_carrier (pf_type_of gl t) with
-            ACSetoid sa -> sa
-          | ACLeibniz _ -> raise Use_replace)
-     | Some h ->
-        let hypt = pf_type_of gl h in
-        let (heq, hargs) = decompose_app hypt in
-        let rec get_all_but_last_two =
-         function
-            []
-          | [_] -> assert false
-          | [_;_] -> []
-          | he::tl -> he::(get_all_but_last_two tl) in
-        let aeq = mkApp (heq,(Array.of_list (get_all_but_last_two hargs))) in
-         try
-          setoid_table_find aeq
-         with Not_found ->
-          errorlabstrm "Setoid_rewrite"
-           (prterm aeq ++ str " is not a setoid equality.")
-   in
-    Toreplace sa
+  if eq_constr t in_c then
+    Toreplace
   else
     match kind_of_term in_c with
       | App (c,al) -> 
-	  let a = Array.map (aux t) al in
-	  let mor =
-           lazy
-            (try
-              begin
-               match morphism_table_find c with
-                  [] -> assert false
-                | morphism::tl ->
-                   if tl <> [] then
-                    msg_warning
-                     (str "There are several morphisms declared for " ++
-                       prterm c ++
-                       str ". The morphism " ++ prmorphism c morphism ++
-                       str " is randomly chosen.") ;
-                   ACMorphism (setoid_morphism_of_constr_morphism morphism)
-              end
-             with Not_found ->
-              let env = Global.env() in
-              let typeofc = (Typing.type_of env Evd.empty c) in
-              let typ = nf_betaiota typeofc in
-              let (argsrev, output) = decompose_prod typ in
-              ACFunction
-               {f_args=List.rev (List.map snd argsrev); f_output=output})
-          in
-	   if (get_mark a) then MApp (mor,a) else Tokeep
+          let a = Array.map (aux t) al in
+           if not (get_mark a) then Tokeep in_c
+           else
+            let mor =
+              try
+                begin
+                 match morphism_table_find c with
+                    [] -> assert false
+                  | morphism::tl ->
+                     if tl <> [] then
+                      msg_warning
+                       (str "There are several morphisms declared for " ++
+                         prterm c ++
+                         str ". The morphism " ++ prmorphism c morphism ++
+                         str " is randomly chosen.") ;
+                     Some
+                      (ACMorphism
+                       (relation_morphism_of_constr_morphism morphism))
+                end
+               with Not_found -> None
+            in
+             (match mor with
+                 Some mor -> MApp (c,mor,a)
+               | None ->
+                 (* the tactic works only if the function type is
+                    made of non-dependent products only. However, here we
+                    can cheat a bit by partially istantiating c to match
+                    the requirement when the arguments to be replaced are
+                    bound by non-dependent products only. *)
+                 let env = Global.env() in
+                 let typeofc = (Typing.type_of env Evd.empty c) in
+                 let typ = nf_betaiota typeofc in
+                 let rec find_non_dependent_function env c c_args_rev typ
+                          f_args_rev a_rev=
+                  function
+                     [] ->
+                      let mor =
+                       ACFunction {f_args=List.rev f_args_rev ; f_output=typ} in
+                      let func = beta_expand c c_args_rev in
+                       MApp (func,mor,Array.of_list (List.rev a_rev))
+                   | (he::tl) as a->
+                      let typnf = Reduction.whd_betadeltaiota env typ in
+                       match kind_of_term typnf with
+                         Cast (typ,_) ->
+                          find_non_dependent_function env c c_args_rev typ
+                           f_args_rev a_rev a
+                       | Prod (name,s,t) ->
+                          let env' = push_rel (name,None,s) env in
+                          begin
+                           match noccurn 1 t, he with
+                              _, Tokeep arg ->
+                               (* generic product, to keep *)
+                               find_non_dependent_function
+                                env' c ((Toapply arg)::c_args_rev)
+                                (subst1 arg t) f_args_rev a_rev tl
+                            | true, _ ->
+                               (* non-dependent product, to replace *)
+                               find_non_dependent_function
+                                env' c ((Toexpand (name,s))::c_args_rev)
+                                 (lift 1 t) (s::f_args_rev) (he::a_rev) tl
+                            | false, _ ->
+                               (* dependent product, to replace *)
+                               (*CSC: this limitation is due to the reflexive
+                                 implementation and it is hard to lift *)
+                               errorlabstrm "Setoid_replace"
+                                (str "Cannot rewrite in the argument of a " ++
+                                 str "dependent product. If you need this " ++
+                                 str "feature, please report to the authors.")
+                          end
+                       | _ -> assert false
+                 in
+                  find_non_dependent_function env c [] typ [] []
+                   (Array.to_list a))
       | Prod (_, c1, c2) -> 
-	  if (dependent (mkRel 1) c2)
-	  then Tokeep
-	  else 
-	    let c1m = aux t c1 in
-	    let c2m = aux t c2 in
-	      if ((is_to_replace c1m)||(is_to_replace c2m))
-	      then (Mimp (c1m, c2m))
-	      else Tokeep
-      | _ -> Tokeep
+          if (dependent (mkRel 1) c2)
+          then Tokeep in_c
+          else 
+            let c1m = aux t c1 in
+            let c2m = aux t c2 in
+              if ((is_to_replace c1m)||(is_to_replace c2m))
+              then (Mimp (c1m, c2m))
+              else Tokeep in_c
+      | _ -> Tokeep in_c
+ in aux t in_c
+
+let cic_morphism_context_list_of_list hole_relation =
+ let rec aux =
+  function
+     [] -> assert false
+   | [out,value] ->
+      mkApp ((Lazy.force coq_singl), [| Lazy.force coq_Relation_Class ; out |]),
+      mkApp ((Lazy.force coq_fcl_singl), [| hole_relation; out ; value |])
+   | (out,value)::tl ->
+      let outtl, valuetl = aux tl in
+       mkApp ((Lazy.force coq_cons),
+        [| Lazy.force coq_Relation_Class ; out ; outtl |]),
+       mkApp ((Lazy.force coq_fcl_cons),
+        [| hole_relation ; out ; outtl ; value ; valuetl |])
  in aux
 
-let create_args ca ma args c1 c2 = 
-  let rec aux i = function
-    | [] -> []
-    | (ACSetoid _)::tl -> 
-	if is_to_replace ma.(i)
-	then (replace_term c1 c2 ca.(i))::ca.(i)::(aux (i+1) tl)
-	else ca.(i)::ca.(i)::(aux (i+1) tl)
-    | (ACLeibniz _)::tl ->
-        if is_to_replace ma.(i)
-        then
-         let newarg = replace_term c1 c2 ca.(i) in
-          newarg::(aux (i+1) tl)
-        else ca.(i)::(aux (i+1) tl)
-  in
-    aux 0 args
-
-let res_tac sa c hyp glll =
-  let fin = match hyp with
-    | None -> Auto.full_trivial
-    | Some h -> 
-	tclORELSE (tclTHEN (tclTRY (apply h)) (tclFAIL 0 "")) 
-	(tclORELSE (tclTHEN (tclTRY (tclTHEN (apply (mkApp ((Lazy.force coq_seq_sym), [|sa.set_a; sa.set_aeq; sa.set_th|]))) (apply h))) (tclFAIL 0 ""))
-	   Auto.full_trivial)
+let rec cic_type_nelist_of_list =
+ function
+    [] -> assert false
+  | [value] ->
+      mkApp ((Lazy.force coq_singl), [| mkType (Termops.new_univ ()) ; value |])
+  | value::tl ->
+     mkApp ((Lazy.force coq_cons),
+      [| mkType (Termops.new_univ ()); value; cic_type_nelist_of_list tl |])
+
+let syntactic_but_representation_of_marked_but hole_relation =
+ let rec aux out =
+  function
+     MApp (f, m, args) ->
+      let morphism_theory, relations =
+       match m with
+          ACMorphism { args = args ; lem = lem } -> lem,args
+        | ACFunction { f_args = f_args ; f_output = f_output } ->
+           let mt =
+            if eq_constr out (cic_relation_class_of_relation_class
+              (Lazy.force coq_prop_relation))
+            then
+              mkApp ((Lazy.force coq_morphism_theory_of_predicate),
+               [| cic_type_nelist_of_list f_args; f|])
+            else
+              mkApp ((Lazy.force coq_morphism_theory_of_function),
+               [| cic_type_nelist_of_list f_args; f_output; f|])
+           in
+            mt,List.map (fun x -> ACLeibniz x) f_args in
+      let cic_relations =
+       List.map cic_relation_class_of_relation_class relations in
+      let cic_args_relations,argst =
+       cic_morphism_context_list_of_list hole_relation
+        (List.combine cic_relations
+          (List.map2 (fun t v -> aux t v) cic_relations
+           (Array.to_list args)))
+      in
+       mkApp ((Lazy.force coq_App),
+        [|hole_relation ; cic_args_relations ; out ; morphism_theory ; argst|])
+   | Toreplace ->
+      mkApp ((Lazy.force coq_Toreplace), [| hole_relation |])
+   | Tokeep c ->
+       mkApp ((Lazy.force coq_Tokeep), [| hole_relation ; out ; c |])
+   | Mimp (source, target) ->
+      mkApp ((Lazy.force coq_Imp),
+       [| hole_relation ; aux out source ; aux out target |])
+ in aux
+
+let apply_coq_setoid_rewrite hole_relation c1 c2 (lft2rgt,h) m =
+ let {refl_aeq=hole_equality; refl_sym=hole_symmetry} = hole_relation in
+ let hole_relation =
+  cic_relation_class_of_relation_class (ACReflexive hole_relation) in
+ let prop_relation =
+  cic_relation_class_of_relation_class (Lazy.force coq_prop_relation) in
+ let hyp =
+  if lft2rgt then h else
+   match hole_symmetry with
+      Some sym ->
+       mkApp (sym, [| c2 ; c1 ; h |])
+    | None ->
+       errorlabstrm "Setoid_rewrite"
+        (str "Rewriting from right to left not permitted since the " ++
+         str "relation " ++ prterm hole_equality ++ str " is not known " ++
+         str "to be symmetric. Either declare it as a symmetric " ++
+         str "relation or use setoid_replace or (setoid_)rewrite from " ++
+         str "left to right only.")
+ in
+  mkApp ((Lazy.force coq_setoid_rewrite),
+   [| hole_relation ; prop_relation ; c1 ; c2 ;
+      syntactic_but_representation_of_marked_but hole_relation
+       prop_relation m ; hyp |])
+
+let relation_rewrite c1 c2 (lft2rgt,cl) gl =
+ let but = pf_concl gl in
+ let (hyp,c1,c2) =
+  let (cl',_) = Clenv.unify_to_subterm cl (c1,but) in
+  let c1 = Clenv.clenv_instance_term cl' c1 in
+  let c2 = Clenv.clenv_instance_term cl' c2 in
+   (lft2rgt,Clenv.clenv_instance_template cl'), c1, c2
+ in
+  let input_relation = relation_of_hypothesis_and_term_to_rewrite gl hyp c1 in
+  let marked_but = mark_occur c1 but in
+  let th =
+   apply_coq_setoid_rewrite input_relation c1 c2 hyp marked_but
   in
-    tclORELSE (tclTHEN (tclTRY (apply (mkApp ((Lazy.force coq_seq_refl), [|sa.set_a; sa.set_aeq; sa.set_th;c|])))) (tclFAIL 0 ""))
-      (tclORELSE assumption
-	 (tclORELSE (tclTHEN (tclTRY (apply (mkApp ((Lazy.force coq_seq_sym), [|sa.set_a; sa.set_aeq; sa.set_th|])))) assumption)
-	    fin))
-
-let id_res_tac (*c*) sa = 
- (apply (mkApp ((Lazy.force coq_seq_refl), [|sa.set_a; sa.set_aeq; sa.set_th(*; c*)|])))
-
-(* An exception to catchs errors *)
-
-exception Nothing_found of constr;;
-
-(* special case of replace_where_needed_gen where all the arguments
-   are of class (ACLeibniz _) *)
-let rec replace_where_needed hyp ca ma c1 c2 = 
-  let rec aux i = function
-    | [] -> tclIDTAC
-    | he::tl ->
-      if is_to_replace he then
-       let dummy = mkProp in (* dummy will never be used *)
+   let thty = pf_type_of gl th in
+   let simplified_thty =
+    pf_unfoldn [[], Lazy.force coq_iff] gl
+     (pf_unfoldn [[], Lazy.force coq_relation_of_relation_class] gl thty)
+   in
+    let ty1,ty2 =
+     match destApplication simplified_thty with
+        (_ (*and*),[|ty1;ty2|]) -> ty1,ty2
+      | _ -> assert false
+    in
+     let th' = mkApp ((Lazy.force coq_proj2), [|ty1; ty2; th|]) in
+     let hyp2 = Termops.replace_term c1 c2 but in
+     let simplified_thty' = mkProd (Anonymous, hyp2, lift 1  but) in
+      (*CSC: the next line does not work because simplified_thty' is not
+        used to generate the type of the new goals ;-(
+      Tactics.apply (mkCast (th',simplified_thty')) gl
+        Thus I am using the following longer (and less accurate) code *)
        tclTHENS
-        (!replace ca.(i) (replace_term c1 c2 ca.(i)))
-        [aux (i+1) tl; zapply (Some(ACLeibniz dummy)) false ca.(i) he c1 c2 hyp]
-      else
-       (aux (i+1) tl)
-  in
-   aux 0 ma
-and replace_where_needed_gen hyp ca ma args c1 c2 =
-  let rec aux i = function
-    | [] -> tclIDTAC
-    | ((ACLeibniz _) as he)::tl ->
-       if is_to_replace ma.(i) then
-        tclTHENS
-         (!replace ca.(i) (replace_term c1 c2 ca.(i)))
-         [aux (i+1) tl ; zapply (Some he) false ca.(i) ma.(i) c1 c2 hyp ]
-       else
-        aux (i+1) tl
-    | (ACSetoid _)::tl -> aux (i+1) tl
-  in
-   aux 0 args
-and create_tac_list i a al c1 c2 hyp = function
-  | [] -> []
-  | (ACLeibniz _)::tl -> create_tac_list (i+1) a al c1 c2 hyp tl
-  | ((ACSetoid setoid) as he)::tl -> 
-      if (is_to_replace a.(i))
-      then (zapply (Some he) false al.(i) a.(i) c1 c2 hyp)::(create_tac_list (i+1) a al c1 c2 hyp tl)
-      else (id_res_tac (*al.(i)*) setoid)::(create_tac_list (i+1) a al c1 c2 hyp tl)
-
-and zapply close is_r gl gl_m c1 c2 hyp glll =
- (match ((kind_of_term gl), gl_m) with
-  | ((App (c,al)),(MApp (m,a))) ->
-     (match Lazy.force m with
-         ACMorphism m ->
-	  let args = Array.of_list (create_args al a m.args c1 c2) in
-           tclTHENS
-            (replace_where_needed_gen hyp al a m.args c1 c2)
-	    [if is_r
-	     then tclTHENS (apply (mkApp (m.lem, args)))
-	       ((create_tac_list 0 a al c1 c2 hyp m.args)@[tclIDTAC])
- 	     else
-              match m.lem2 with
-                 None -> 
-                  tclTHENS (apply (mkApp (m.lem, args)))
-                   (create_tac_list 0 a al c1 c2 hyp m.args)
-               | Some xom -> 
-                  tclTHENS (apply (mkApp (xom, args)))
-                   (create_tac_list 0 a al c1 c2 hyp m.args)]
-       | ACFunction f ->
-          tclTHENS
-           (replace_where_needed hyp al (Array.to_list a) c1 c2)
-           [match close with
-               None -> tclIDTAC
-             | Some (ACLeibniz _) -> reflexivity
-             | Some (ACSetoid setoid) -> id_res_tac setoid])
-  | ((Prod (_,hh, cc)),(Mimp (hhm, ccm))) ->
-      let al = [|hh; cc|] in
-      let a = [|hhm; ccm|] in
-      let fleche_constr = (Lazy.force coq_fleche) in
-      let fleche_cp = destConst fleche_constr in
-      let new_concl = (mkApp (fleche_constr, al)) in
-      let m = find_morphism_fleche () in
-	if is_r 
-	then
-	  let args = Array.of_list (create_args al a m.args c1 c2) in  
-	    tclTHEN (change_in_concl None new_concl)
-	      (tclTHENS (apply (mkApp (m.lem, args)))
-		 ((create_tac_list 0 a al c1 c2 hyp m.args)@[unfold_constr (ConstRef fleche_cp)]))
-	else
-         (zapply (Some m.output) is_r new_concl
-           (MApp (lazy (ACMorphism m),a)) c1 c2 hyp)
-  | (_, Toreplace setoid) -> 
-      if is_r 
-      then (match hyp with
-	      | None -> errorlabstrm "Setoid_replace"
-		  (str "You should use the tactic Replace here")
-	      | Some h ->
-		  let hypt = pf_type_of glll h in
-		  let (heq, hargs) = decompose_app hypt in
-		  let rec get_last_two = function
-		    | [c1;c2] -> (c1, c2)
-		    | x::y::z -> get_last_two (y::z)
-		    | _ -> assert false in
-		  let (hc1,hc2) = get_last_two hargs in
-		    if c1 = hc1
-		    then 				     
-		      apply (mkApp (Lazy.force coqproj2,[|(mkArrow hc1 hc2);(mkArrow hc2 hc1);h|]))
-		    else 
-		      apply (mkApp (Lazy.force coqproj1,[|(mkArrow hc1 hc2);(mkArrow hc2 hc1);h|]))
-	   )
-      else (res_tac setoid gl hyp glll)
-  | (_, Tokeep) -> (match hyp with 
-		      | None -> errorlabstrm "Setoid_replace"
-			  (str "No replacable occurence of " ++ prterm c1 ++ str " found")
-		      | Some _ ->errorlabstrm "Setoid_replace"
-			  (str "No rewritable occurence of " ++ prterm c1 ++ str " found"))
-  | _ -> assert false) glll
-
-let setoid_replace c1 c2 hyp gl =
-  let but = (pf_concl gl) in
-   try
-    (zapply None true but (mark_occur gl hyp c1 but) c1 c2 hyp) gl
-   with
-    Use_replace -> (!replace c1 c2) gl
+        (Tactics.apply (mkCast (th',simplified_thty')))
+        [Tactics.change_in_concl None hyp2] gl
+     (*CSC: this is another way to proceed, but the generated proof_term
+       would be much bigger than possible
+      Tactics.forward true Anonymous (mkCast (th',simplified_thty')) gl
+      (... followed by the application of the introduced hypothesis ...)
+     *)
 
 let general_s_rewrite lft2rgt c gl =
-  let ctype = pf_type_of gl c in
-  let (equiv, args) = decompose_app ctype in
-  let rec get_last_two = function
-    | [c1;c2] -> (c1, c2)
-    | x::y::z -> get_last_two (y::z)
-    | _ -> error "The term provided is not an equivalence" in 
-  let (c1,c2) = get_last_two args in
-    if lft2rgt
-    then setoid_replace c1 c2 (Some c) gl
-    else setoid_replace c2 c1 (Some c) gl
-
-let setoid_replace c1 c2 = setoid_replace c1 c2 None
+ let (wc,_)  = Evar_refiner.startWalk gl in
+ let ctype = pf_type_of gl c in
+ let eqclause  =
+  Clenv.make_clenv_binding wc (c,ctype) Rawterm.NoBindings in
+ let (equiv, args) =
+  decompose_app (Clenv.clenv_instance_template_type eqclause) in
+ let rec get_last_two = function
+   | [c1;c2] -> (c1, c2)
+   | x::y::z -> get_last_two (y::z)
+   | _ -> error "The term provided is not an equivalence" in
+ let (c1,c2) = get_last_two args in
+   if lft2rgt
+   then relation_rewrite c1 c2 (lft2rgt,eqclause) gl
+   else relation_rewrite c2 c1 (lft2rgt,eqclause) gl
+
+exception Use_replace
+
+(*CSC: the name should be changed *)
+let setoid_replace c1 c2 gl =
+ try
+  let relation =
+   match default_relation_for_carrier (pf_type_of gl c1) with
+      ACReflexive sa -> sa
+    | ACLeibniz _ -> raise Use_replace
+  in
+   let eq = mkApp (relation.refl_aeq, [| c1 ; c2 |]) in
+    tclTHENS (assert_tac false Anonymous eq)
+      [onLastHyp (fun id ->
+        tclTHEN
+          (general_s_rewrite true (mkVar id))
+          (clear [id]));
+       Tacticals.tclIDTAC] gl
+ with
+  Use_replace -> (!replace c1 c2) gl
 
 let setoid_rewriteLR = general_s_rewrite true
 
diff --git a/tactics/setoid_replace.mli b/tactics/setoid_replace.mli
index 02046c55b..e41728ead 100644
--- a/tactics/setoid_replace.mli
+++ b/tactics/setoid_replace.mli
@@ -27,6 +27,9 @@ val setoid_rewriteRL : constr -> tactic
 
 val general_s_rewrite : bool -> constr -> tactic
 
+val add_relation :
+ constr_expr -> constr_expr -> constr_expr option -> constr_expr option -> unit
+
 val add_setoid : constr_expr -> constr_expr -> constr_expr -> unit
 
 val new_named_morphism : Names.identifier -> constr_expr -> unit
diff --git a/theories/Setoids/Setoid.v b/theories/Setoids/Setoid.v
index bca2bf9de..bf54f0567 100644
--- a/theories/Setoids/Setoid.v
+++ b/theories/Setoids/Setoid.v
@@ -1,3 +1,4 @@
+
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
 (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
@@ -8,64 +9,345 @@
 
 (*i $Id$: i*)
 
-Section Setoid.
+Set Implicit Arguments.
+
+(* DEFINITIONS OF Relation_Class AND n-ARY Morphism_Theory *)
+
+Definition is_reflexive (A: Type) (Aeq: A -> A -> Prop) : Prop :=
+ forall x:A, Aeq x x.
+
+Definition is_symmetric (A: Type) (Aeq: A -> A -> Prop) : Prop :=
+ forall (x y:A), Aeq x y -> Aeq y x.
+
+Inductive Relation_Class : Type :=
+   Reflexive : forall A Aeq, (@is_reflexive A Aeq) -> Relation_Class
+ | Leibniz : Type -> Relation_Class.
+
+Implicit Type Hole Out: Relation_Class.
+
+Definition carrier_of_relation_class : Relation_Class -> Type.
+ intro; case X; intros.
+ exact A.
+ exact T.
+Defined.
+
+Inductive nelistT (A : Type) : Type :=
+   singl : A -> (nelistT A)
+ | cons : A -> (nelistT A) -> (nelistT A).
+
+Implicit Type In: (nelistT Relation_Class).
+
+Definition function_type_of_morphism_signature :
+ (nelistT Relation_Class) -> Relation_Class -> Type.
+  intros In Out.
+  induction In.
+    exact (carrier_of_relation_class a -> carrier_of_relation_class Out).
+    exact (carrier_of_relation_class a -> IHIn).
+Defined. 
+
+Definition make_compatibility_goal_aux:
+ forall In Out
+  (f g: function_type_of_morphism_signature In Out), Prop.
+ intros; induction In; simpl in f, g.
+   induction a; destruct Out; simpl in f, g.
+     exact (forall (x1 x2: A), (Aeq x1 x2) -> (Aeq0 (f x1) (g x2))).
+     exact (forall (x1 x2: A), (Aeq x1 x2) -> f x1 = g x2).
+     exact (forall (x: T), (Aeq (f x) (g x))).
+     exact (forall (x: T), f x = g x).
+  induction a; simpl in f, g.
+    exact (forall (x1 x2: A), (Aeq x1 x2) -> IHIn (f x1) (g x2)).
+    exact (forall (x: T), IHIn (f x) (g x)).
+Defined. 
+
+Definition make_compatibility_goal :=
+ (fun In Out f => make_compatibility_goal_aux In Out f f).
+
+Record Morphism_Theory In Out : Type :=
+   {Function : function_type_of_morphism_signature In Out;
+    Compat : make_compatibility_goal In Out Function}.
+
+Definition list_of_Leibniz_of_list_of_types:
+ nelistT Type -> nelistT Relation_Class.
+ induction 1.
+   exact (singl (Leibniz a)).
+   exact (cons (Leibniz a) IHX).
+Defined.
+
+(* every function is a morphism from Leibniz+ to Leibniz *)
+Definition morphism_theory_of_function :
+ forall (In: nelistT Type) (Out: Type),
+  let In' := list_of_Leibniz_of_list_of_types In in
+  let Out' := Leibniz Out in
+   function_type_of_morphism_signature In' Out' ->
+    Morphism_Theory In' Out'.
+  intros.
+  exists X.
+  induction In;  unfold make_compatibility_goal; simpl.
+    reflexivity.
+    intro; apply (IHIn (X x)).
+Defined.
+
+(* THE Prop RELATION CLASS *)
+
+Add Relation Prop iff reflexivity proved by iff_refl symmetry proved by iff_sym.
+
+Definition Prop_Relation_Class : Relation_Class.
+ eapply (@Reflexive _ iff).
+ exact iff_refl.
+Defined.
+
+(* every predicate is  morphism from Leibniz+ to Prop_Relation_Class *)
+Definition morphism_theory_of_predicate :
+ forall (In: nelistT Type),
+  let In' := list_of_Leibniz_of_list_of_types In in
+   function_type_of_morphism_signature In' Prop_Relation_Class ->
+    Morphism_Theory In' Prop_Relation_Class.
+  intros.
+  exists X.
+  induction In;  unfold make_compatibility_goal; simpl.
+    intro; apply iff_refl.
+    intro; apply (IHIn (X x)).
+Defined.
+
+(* THE CIC PART OF THE REFLEXIVE TACTIC (SETOID REWRITE) *)
+
+Inductive Morphism_Context Hole : Relation_Class -> Type :=
+    App : forall In Out,
+                Morphism_Theory In Out ->  Morphism_Context_List Hole In ->
+                  Morphism_Context Hole Out
+  | Toreplace : Morphism_Context Hole Hole
+  | Tokeep :
+     forall (S: Relation_Class),
+      carrier_of_relation_class S -> Morphism_Context Hole S
+  | Imp :
+      Morphism_Context Hole Prop_Relation_Class ->
+       Morphism_Context Hole Prop_Relation_Class ->
+        Morphism_Context Hole Prop_Relation_Class
+with Morphism_Context_List Hole: nelistT Relation_Class -> Type :=
+    fcl_singl :
+      forall (S: Relation_Class), Morphism_Context Hole S ->
+       Morphism_Context_List Hole (singl S)
+ | fcl_cons :
+      forall (S: Relation_Class) (L: nelistT Relation_Class),
+       Morphism_Context Hole S -> Morphism_Context_List Hole L ->
+        Morphism_Context_List Hole (cons S L).
+
+Scheme Morphism_Context_rect2 := Induction for Morphism_Context  Sort Type
+with Morphism_Context_List_rect2 := Induction for Morphism_Context_List Sort Type.
+
+Inductive prodT (A B: Type) : Type :=
+ pairT : A -> B -> prodT A B.
+
+Definition product_of_relation_class_list : nelistT Relation_Class -> Type.
+ induction 1.
+   exact (carrier_of_relation_class a).
+   exact (prodT (carrier_of_relation_class a) IHX).
+Defined.
 
-Variable A : Type.
-Variable Aeq : A -> A -> Prop.
+Definition relation_of_relation_class:
+ forall Out,
+  carrier_of_relation_class Out -> carrier_of_relation_class Out -> Prop.
+ destruct Out.
+   exact Aeq.
+   exact (@eq T).
+Defined.
 
-Record Setoid_Theory : Prop := 
+Definition relation_of_product_of_relation_class_list:
+ forall In,
+  product_of_relation_class_list In -> product_of_relation_class_list In -> Prop.
+ induction In.
+   exact (relation_of_relation_class a).
+
+   simpl; intros.
+   destruct X; destruct X0.
+   exact (relation_of_relation_class a c c0 /\ IHIn p p0).
+Defined. 
+
+Definition apply_morphism:
+ forall In Out (m: function_type_of_morphism_signature In Out)
+  (args: product_of_relation_class_list In), carrier_of_relation_class Out.
+ intros.
+ induction In.
+   exact (m args).
+   simpl in m, args.
+   destruct args.
+   exact (IHIn (m c) p).
+Defined.
+
+Theorem apply_morphism_compatibility:
+ forall In Out (m1 m2: function_type_of_morphism_signature In Out)
+   (args1 args2: product_of_relation_class_list In),
+     make_compatibility_goal_aux _ _ m1 m2 ->
+      relation_of_product_of_relation_class_list _ args1 args2 ->
+        relation_of_relation_class _
+         (apply_morphism _ _ m1 args1)
+         (apply_morphism _ _ m2 args2).
+  intros.
+  induction In.
+    simpl; simpl in m1, m2, args1, args2, H0.
+    destruct a; destruct Out.
+      apply H; exact H0.
+      simpl; apply H; exact H0.
+      simpl; rewrite H0; apply H.
+      simpl; rewrite H0; apply H.
+   simpl in args1, args2, H0.
+   destruct args1; destruct args2; simpl.
+   destruct H0.
+   simpl in H.
+   destruct a; simpl in H.
+     apply IHIn.
+       apply H; exact H0.
+       exact H1.
+    rewrite H0; apply IHIn.
+      apply H.
+      exact H1.
+Qed.
+
+Definition interp :
+ forall Hole Out, carrier_of_relation_class Hole ->
+  Morphism_Context Hole Out -> carrier_of_relation_class Out.
+ intros Hole Out H t.
+ elim t using
+  (@Morphism_Context_rect2 Hole (fun S _ => carrier_of_relation_class S)
+    (fun L fcl => product_of_relation_class_list L));
+  intros.
+   exact (apply_morphism _ _ (Function m) X).
+   exact H.
+   exact c.
+   exact (X -> X0).
+   exact X.
+   split; [ exact X | exact X0 ].
+Defined.
+
+(*CSC: interp and interp_relation_class_list should be mutually defined, since
+   the proof term of each one contains the proof term of the other one. However
+   I cannot do that interactively (I should write the Fix by hand) *)
+Definition interp_relation_class_list :
+ forall Hole (L: nelistT Relation_Class), carrier_of_relation_class Hole ->
+  Morphism_Context_List Hole L -> product_of_relation_class_list L.
+ intros Hole L H t.
+ elim t using
+  (@Morphism_Context_List_rect2 Hole (fun S _ => carrier_of_relation_class S)
+    (fun L fcl => product_of_relation_class_list L));
+ intros.
+   exact (apply_morphism _ _ (Function m) X).
+   exact H.
+   exact c.
+   exact (X -> X0).
+   exact X.
+   split; [ exact X | exact X0 ].
+Defined.
+
+Theorem setoid_rewrite:
+ forall Hole Out (E1 E2: carrier_of_relation_class Hole)
+  (E: Morphism_Context Hole Out),
+   (relation_of_relation_class Hole E1 E2) ->
+    (relation_of_relation_class Out (interp E1 E) (interp E2 E)).
+ intros.
+ elim E using
+   (@Morphism_Context_rect2 Hole
+     (fun S E => relation_of_relation_class S (interp E1 E) (interp E2 E))
+     (fun L fcl =>
+       relation_of_product_of_relation_class_list _
+        (interp_relation_class_list E1 fcl)
+        (interp_relation_class_list E2 fcl)));
+ intros.
+   change (relation_of_relation_class Out0
+    (apply_morphism _ _ (Function m) (interp_relation_class_list E1 m0))
+    (apply_morphism _ _ (Function m) (interp_relation_class_list E2 m0))).
+   apply apply_morphism_compatibility.
+     exact (Compat m).
+     exact H0.
+
+   exact H.
+
+   unfold interp, Morphism_Context_rect2.
+   (*CSC: reflexivity used here*)
+   destruct S.
+     apply i.
+     simpl; reflexivity.
+
+   change
+     (relation_of_relation_class Prop_Relation_Class
+       (interp E1 m -> interp E1 m0) (interp E2 m -> interp E2 m0)).
+   simpl; simpl in H0, H1.
+   tauto.
+
+  exact H0.
+
+  change
+    (relation_of_relation_class _ (interp E1 m) (interp E2 m) /\
+     relation_of_product_of_relation_class_list _
+       (interp_relation_class_list E1 m0) (interp_relation_class_list E2 m0)).
+   split.
+     exact H0.
+     exact H1.
+Qed.
+
+(* BEGIN OF UTILITY/BACKWARD COMPATIBILITY PART *)
+
+Record Setoid_Theory  (A: Type) (Aeq: A -> A -> Prop) : Prop := 
   {Seq_refl : forall x:A, Aeq x x;
    Seq_sym : forall x y:A, Aeq x y -> Aeq y x;
    Seq_trans : forall x y z:A, Aeq x y -> Aeq y z -> Aeq x z}.
 
-End Setoid.
+Definition relation_class_of_setoid_theory:
+ forall (A: Type) (Aeq: A -> A -> Prop),
+  Setoid_Theory Aeq -> Relation_Class.
+ intros.
+ apply (@Reflexive _ Aeq).
+ exact (Seq_refl H).
+Defined.
 
-Definition Prop_S : Setoid_Theory Prop iff.
-split; [ exact iff_refl | exact iff_sym | exact iff_trans ].
-Qed.
+Definition equality_morphism_of_setoid_theory:
+ forall (A: Type) (Aeq: A -> A -> Prop) (ST: Setoid_Theory Aeq),
+   let ASetoidClass := relation_class_of_setoid_theory ST in 
+    (Morphism_Theory (cons ASetoidClass (singl ASetoidClass))
+      Prop_Relation_Class).
+ intros.
+ exists Aeq.
+ pose (sym   := Seq_sym ST);  clearbody sym.
+ pose (trans := Seq_trans ST); clearbody trans.
+ (*CSC: symmetry and transitivity used here *)
+ unfold make_compatibility_goal; simpl; split; eauto.
+Defined.
 
-Add Setoid Prop iff Prop_S.
+(* END OF UTILITY/BACKWARD COMPATIBILITY PART *)
 
-Hint Resolve (Seq_refl Prop iff Prop_S): setoid.
-Hint Resolve (Seq_sym Prop iff Prop_S): setoid.
-Hint Resolve (Seq_trans Prop iff Prop_S): setoid.
+(* A FEW EXAMPLES *)
 
-Add Morphism or : or_ext.
-intros.
-inversion H1.
-left.
-inversion H.
-apply (H3 H2).
+Add Morphism iff : Iff_Morphism.
+ tauto.
+Defined.
 
-right.
-inversion H0.
-apply (H3 H2).
-Qed.
+(* impl IS A MORPHISM *)
 
-Add Morphism and : and_ext.
-intros.
-inversion H1.
-split.
-inversion H.
-apply (H4 H2).
+Definition impl (A B: Prop) := A -> B.
 
-inversion H0.
-apply (H4 H3).
-Qed.
+Add Morphism impl : Impl_Morphism.
+unfold impl; tauto.
+Defined.
 
-Add Morphism not : not_ext.
-red in |- *; intros.
-apply H0.
-inversion H.
-apply (H3 H1).
-Qed.
+(* and IS A MORPHISM *)
 
-Definition fleche (A B:Prop) := A -> B.
+Add Morphism and : And_Morphism.
+ tauto.
+Defined.
 
-Add Morphism fleche : fleche_ext.
-unfold fleche in |- *.
-intros.
-inversion H0.
-inversion H.
-apply (H3 (H1 (H6 H2))).
-Qed.
+(* or IS A MORPHISM *)
+
+Add Morphism or : Or_Morphism.
+ tauto.
+Defined.
+
+(* not IS A MORPHISM *)
+
+Add Morphism not : Not_Morphism.
+ tauto.
+Defined.
+
+(* FOR BACKWARD COMPATIBILITY *)
+Implicit Arguments Setoid_Theory [].
+Implicit Arguments Seq_refl [].
+Implicit Arguments Seq_sym [].
+Implicit Arguments Seq_trans [].