Major bug fixing and improvement of the setoid_{replace,rewrite} tactics:

1. setoid and morphisms declaration were used to become in scope only
   when a module is imported (and to disappear when a module is closed).
   Thus it was possible to declare a setoid in a module A; a morphism on
   it in a module B that imports A; and to write a module C that imports
   B (but not A) that uses the morphism. Since the morphism is in scope
   but the setoid isn't this was a source of bugs.
   Fixed by making the setoid/morphisms declaration always in scope
   (i.e. they become in scope when the module is loaded, not when it is
   imported).
2. since it is possible to define different setoids for the same type
   / different morphisms on the same function  in separate modules and
   since it is possible to import them at once, we must allow the possibility
   to have more than one setoid for each type and more than one morphism
   for each function. The data structures of the tactic has been completely
   revised to allow this possibility. Right now warnings are used to
   highlight situations when an ambiguity is arised. In the near future
   syntax will be added to disambiguate the situation, and smart algorithms
   to find the right interpretations when more than one applies but only
   a few are succesfull. For the moment the choice of the interpretation
   (i.e. the association of a morphism to each function in the goal)
   is already done before the actual start of the tactic (in order to
   allow a modular implementation of the choice of the interpretation).
3. the tactic used to work only in those situations where all the functions
   involved in the path(s) root of the term - term(s) to replace were
   morphisms. In the case where they are simple functions (i.e. the
   ``default setoid'' is Leibniz) the tactic failed. These cases are now
   considered by making the setoid_replace tactic perform simple replace steps
   where needed. A future optimization will allow to minimize the number
   of replace steps.

The tactic should be 100% compatible with the old tactic, but for the
situations that used to fail and are now succesfull.
The declaration of setoids/morphisms can now also be succesfull where it
used to fail.


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

2 files changed, 448 insertions, 238 deletions

diff --git a/tactics/setoid_replace.ml b/tactics/setoid_replace.ml
index 0a35282b7..44203278b 100644
--- a/tactics/setoid_replace.ml
+++ b/tactics/setoid_replace.ml
@@ -30,19 +30,46 @@ open Nametab
 open Decl_kinds
 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 morphism =
+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 'a morphism =
     { lem : constr;
-      profil : bool list;
-      arg_types : constr list;
+      args : 'a setoid_class list;
+      output : 'a setoid_class;
       lem2 : constr option
     }
 
+type funct =
+    { f_args : constr list;
+      f_output : constr
+    }
+
+type morphism_class =
+   ACMorphism of setoid morphism
+ | ACFunction of funct
+
+let subst_mps_in_setoid_class subst =
+ function
+    ACSetoid  t -> ACSetoid  (subst_mps subst t)
+  | ACLeibniz t -> ACLeibniz (subst_mps subst t) 
+
+let constr_setoid_class_of_setoid_setoid_class =
+ function
+    ACSetoid setoid -> ACSetoid setoid.set_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
@@ -53,7 +80,7 @@ let current_constant id =
   try
     global_reference id
   with Not_found ->
-    anomaly ("Setoid: cannot find "^(string_of_id id))
+    anomaly ("Setoid: cannot find " ^ (string_of_id id))
 
 (* Setoid_theory *)
 
@@ -67,6 +94,8 @@ let coq_fleche = lazy(constant ["Setoid"] "fleche")
 
 (* Coq constants *)
 
+let coqiff = lazy(global_constant ["Logic"] "iff")
+
 let coqeq = lazy(global_constant ["Logic"] "eq")
 
 let coqconj = lazy(global_constant ["Logic"] "conj")
@@ -79,14 +108,56 @@ let coqproj2 = lazy(global_constant ["Logic"] "proj2")
 
 (* Setoids are stored in a table which is synchronised with the Reset mechanism. *)
 
-module Cmap = Map.Make(struct type t = constr let compare = compare end)
-
 let setoid_table = ref Gmap.empty
 
 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 prsetoid s =
+ str "(" ++ prterm s.set_a ++ str "," ++ prterm s.set_aeq ++ str ")"
+
+let prsetoid_class =
+ function
+    ACSetoid eq  ->
+     (try prsetoid (setoid_table_find eq)
+      with Not_found ->
+       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
+
+
+(* A function that gives back the only setoid 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
+    [] -> ACLeibniz a
+  | setoid::tl ->
+     if tl <> [] then
+      msg_warning
+       (str "There are several setoids whose carrier is " ++ prterm a ++
+         str ". The setoid " ++ prsetoid setoid ++
+         str " is randomly chosen.") ;
+     ACSetoid setoid
+
+let setoid_morphism_of_constr_morphism =
+ let setoid_setoid_class_of_constr_setoid_class =
+  function
+     ACLeibniz t -> ACLeibniz t
+   | ACSetoid aeq ->
+      ACSetoid (try setoid_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
+    {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
@@ -109,13 +180,23 @@ let _ =
     { Summary.freeze_function = (fun () -> !setoid_table);
       Summary.unfreeze_function = (fun t -> setoid_table := t);
       Summary.init_function = (fun () -> setoid_table := Gmap .empty);
-      Summary.survive_module = false;
+      Summary.survive_module = true;
       Summary.survive_section = false }
 
 (* Declare a new type of object in the environment : "setoid-theory". *)
 
 let (setoid_to_obj, obj_to_setoid)=
-  let cache_set (_,(s, th)) = setoid_table_add (s,th)
+  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)
   and subst_set (_,subst,(s,th as obj)) =
     let s' = subst_mps subst s in
     let th' = subst_setoid subst th in
@@ -125,7 +206,7 @@ let (setoid_to_obj, obj_to_setoid)=
   in 
     declare_object {(default_object "setoid-theory") with
 		      cache_function = cache_set;
-		      open_function = (fun i o -> if i=1 then cache_set o);
+		      load_function = (fun i o -> cache_set o);
 		      subst_function = subst_set;
 		      classify_function = (fun (_,x) -> Substitute x);
 		      export_function = export_set}
@@ -136,24 +217,63 @@ let (setoid_to_obj, obj_to_setoid)=
 
 let morphism_table = ref Gmap.empty
 
-let morphism_table_add (m,c) = morphism_table := Gmap.add m c !morphism_table
 let morphism_table_find m = Gmap.find m !morphism_table
-let morphism_table_mem m = Gmap.mem m !morphism_table
+let morphism_table_add (m,c) =
+ let old =
+  try
+   morphism_table_find m
+  with
+   Not_found -> []
+ in
+  try
+   let old_morph =
+    List.find
+     (function mor -> mor.args = c.args && mor.output = c.output) old
+   in
+    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" ++
+       str " compatibility was granted by " ++
+       prterm old_morph.lem ++
+       (match old_morph.lem2 with
+          None -> str ""
+        | Some t-> str " and "++ prterm t) ++ 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 arg_types' = list_smartmap (subst_mps subst) morph.arg_types 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
     if lem' == morph.lem
-      && arg_types' == morph.arg_types
+      && args' == morph.args
+      && output' == morph.output
       && lem2' == morph.lem2
     then
       morph
     else
       { lem = lem' ;
-	profil = morph.profil ;
-	arg_types = arg_types' ;
-	lem2 = lem2' ;
+	args = args' ;
+	output = output' ;
+	lem2 = lem2'
       }
 
 
@@ -162,7 +282,7 @@ let _ =
     { Summary.freeze_function = (fun () -> !morphism_table);
       Summary.unfreeze_function = (fun t -> morphism_table := t);
       Summary.init_function = (fun () -> morphism_table := Gmap .empty);
-      Summary.survive_module = false;
+      Summary.survive_module = true;
       Summary.survive_section = false }
 
 (* Declare a new type of object in the environment : "morphism-definition". *)
@@ -178,26 +298,34 @@ let (morphism_to_obj, obj_to_morphism)=
   in 
     declare_object {(default_object "morphism-definition") with
 		      cache_function = cache_set;
-		      open_function = (fun i o -> if i=1 then cache_set o);
+		      load_function = (fun i o -> cache_set o);
 		      subst_function = subst_set;
 		      classify_function = (fun (_,x) -> Substitute x);
 		      export_function = export_set}
 
-(************************** Adding a setoid to the database *********************)
+(************************** Printing setoids and morphisms **********************)
+
+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 ;
+  Gmap.iter
+   (fun k l ->
+     List.iter
+      (fun ({lem=lem ; lem2=lem2} 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 "."))
+      l) !morphism_table
+;;
 
-(* Find the setoid theory associated with a given type A.
-This implies that only one setoid theory can be declared for
-a given type A. *)
+(************************** Adding a setoid to the database *********************)
 
-let find_theory a =
-  try 
-    setoid_table_find a 
-  with Not_found ->
-    errorlabstrm "Setoid" 
-      (str "No Declared Setoid Theory for " ++
-	 prterm a ++ fnl () ++
-	 str "Use Add Setoid to declare it")
-    
 (* Add a Setoid to the database after a type verification. *)
 
 let eq_lem_common_sign env a eq =
@@ -264,15 +392,12 @@ let gen_eq_lem_name =
       make_ident "setoid_eq_ext" (Some !i)
 
 let add_setoid a aeq th =
-  if setoid_table_mem a 
-  then errorlabstrm "Add Setoid"
-    (str "A Setoid Theory is already declared for " ++ prterm a)
-  else let env = Global.env () 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 (Lib.add_anonymous_leaf 
 	    (setoid_to_obj 
-	       (a, { set_a = a;
+	       (aeq, { set_a = a;
 		     set_aeq = aeq;
 		     set_th = th}));
 	  let sym = mkApp ((Lazy.force coq_seq_sym), [|a; aeq; th|]) in
@@ -295,10 +420,10 @@ let add_setoid a aeq th =
 	    let eqmorph = (current_constant eq_ext_name) in
 	    let eqmorph2 = (current_constant eq_ext_name2) in
 	      (Lib.add_anonymous_leaf
-		 (morphism_to_obj (aeq, 
+		 (morphism_to_obj (aeq,
 				   { lem = eqmorph;
-				     profil = [true; true];
-				     arg_types = [a;a];
+                                     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")
@@ -314,8 +439,8 @@ let add_setoid a aeq th =
 
 let edited = ref Gmap.empty
 
-let new_edited id m profil = 
-  edited := Gmap.add id (m,profil)  !edited
+let new_edited id m = 
+  edited := Gmap.add id m !edited
 
 let is_edited id =
   Gmap.mem id !edited
@@ -341,182 +466,175 @@ let gen_lem_name m = match kind_of_term m with
       (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 lisset body n =
-  let l = (List.length lisset) in
+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
-    | true::q -> 
+    | (ACSetoid _)::tl -> 
 	a1.(i) <- (mkRel n);
 	a2.(i) <- (mkRel (n-1));
-	aux (i+1) (n-2) q
-    | false::q ->
+	aux (i+1) (n-2) tl
+    | (ACLeibniz _)::tl ->
 	a1.(i) <- (mkRel n);
 	a2.(i) <- (mkRel n);
-	aux (i+1) (n-1) q
+	aux (i+1) (n-1) tl
     | [] -> () in 
-    aux 0 n lisset;
-    if (eq_constr body mkProp)
+    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 if (setoid_table_mem body)
-    then mkApp ((setoid_table_find body).set_aeq, [|(mkApp (m, a1)); (mkApp (m, a2))|])
-    else mkApp ((Lazy.force coqeq), [|body; (mkApp (m, a1)); (mkApp (m, a2))|])
-
-let gen_lemma_middle m larg lisset body n =
-  let rec aux la li i n = match (la, li) with
-    | ([], []) -> gen_lemma_tail m lisset body n
-    | (t::q, true::lq) -> 
-	mkArrow (mkApp ((setoid_table_find t).set_aeq, 
-			[|(mkRel i); (mkRel (i-1))|])) (aux q lq (i-1) (n+1))
-    | (t::q, false::lq) -> aux q lq (i-1) n
-    | _ -> assert false
-  in aux larg lisset n n
-
-let gen_compat_lemma env m body larg lisset = 
-  let rec aux la li n = match (la, li) with
-    | (t::q, true::lq) -> 
-	prod_create env (t,(prod_create env (t, (aux q lq (n+2)))))
-    | (t::q, false::lq) -> 
-	prod_create env (t, (aux q lq (n+1)))
-    | ([],[]) -> gen_lemma_middle m larg lisset body n
-    | _ -> assert false
-  in aux larg lisset 0
+    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
 
 let new_morphism m id hook =
-  if morphism_table_mem m
-  then errorlabstrm "New Morphism"
-    (str "The term " ++ prterm m ++ str " is already declared as a morphism")
-  else 
-    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 (argsrev, body) = (decompose_prod typ) in
-    let args = (List.rev argsrev) in
-      if (args=[])
-      then errorlabstrm "New Morphism"
-	(str "The term " ++ prterm m ++ str " is not a product")
-      else if (check_is_dependent typ (List.length args))
-      then  errorlabstrm "New Morphism"
-	(str "The term " ++ prterm m ++ str " should not be a dependent product")
-      else (
-	let args_t = (List.map snd args) in
-	let poss = (List.map setoid_table_mem args_t) in
-	let lem = (gen_compat_lemma env m body args_t poss) in
-	new_edited id m poss;
-	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 l1 n = function
+  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 (argsrev, output) = (decompose_prod typ) in
+  let args_ty = (List.map snd (List.rev argsrev)) in
+    if (args_ty=[])
+    then errorlabstrm "New Morphism"
+     (str "The term " ++ prterm m ++ str " is not a product")
+    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
   | [] -> []
-  | true::q -> ((List.hd l1), n)::(sub_bool (List.tl l1) (n-2) q)
-  | false::q -> (sub_bool (List.tl l1) (n-1) q)
+  | (ACSetoid setoid)::tl -> (setoid, n)::(sub_bool (n-2) tl)
+  | (ACLeibniz _)::tl -> (sub_bool (n-1) tl)
 
-let gen_lemma_iff_tail m mext larg lisset n k =
+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 lisset 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
     |[] -> ()
-    |true::q ->
+    |(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) q)
-    |false::q ->
+	aux (i+2) (j-2) tl)
+    |(ACLeibniz _)::tl ->
        (a1.(i) <- (mkRel j);
 	a2.(i) <- (mkRel j);
-	aux (i+1) (j-1) q) in
+	aux (i+1) (j-1) tl) in
   let rec aux2 i j = function
-    | (t,p)::q -> 
-	let th = (setoid_table_find t).set_th
-	and equiv = (setoid_table_find t).set_aeq in
-	  a1.(i) <- (mkRel j);
-	  a2.(i) <- mkApp ((Lazy.force coq_seq_sym),
-			   [|t; equiv; th; (mkRel p); (mkRel (p-1)); (mkRel j)|]);
-	  aux2 (i+1) (j-1) q
+    | ({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
-    | true::q -> 
+    | (ACSetoid _)::tl -> 
 	b1.(i) <- (mkRel j);
 	b2.(i) <- (mkRel (j-1));
-	aux3 (i+1) (j-2) q
-    | false::q ->
+	aux3 (i+1) (j-2) tl
+    | (ACLeibniz _)::tl ->
 	b1.(i) <- (mkRel j);
 	b2.(i) <- (mkRel j);
-	aux3 (i+1) (j-1) q
+	aux3 (i+1) (j-1) tl
     | [] -> () in 
-    aux 0 k lisset;
-    aux2 n (k-n) (sub_bool larg k lisset);
-    aux3 0 k lisset;
+    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 larg lisset n =
-  let rec aux la li i k = match (la, li) with
-    | ([], []) -> gen_lemma_iff_tail m mext larg lisset n k
-    | (t::q, true::lq) -> 
-	lambda_create env ((mkApp ((setoid_table_find t).set_aeq, [|(mkRel i); (mkRel (i-1))|])),
-			   (aux q lq (i-1) (k+1)))
-    | (t::q, false::lq) -> aux q lq (i-1) k
-    | _ -> assert false
-  in aux larg lisset n n
-
-let gen_lem_iff env m mext larg lisset =
-  let rec aux la li n = match (la, li) with
-    | (t::q, true::lq) -> 
-	lambda_create env (t,(lambda_create env (t, (aux q lq (n+2)))))
-    | (t::q, false::lq) -> 
-	lambda_create env (t, (aux q lq (n+1)))
-    | ([],[]) -> gen_lemma_iff_middle env m mext larg lisset n
-    | _ -> assert false
-  in aux larg lisset 0
-
-let add_morphism lem_name (m,profil) =
-  if morphism_table_mem m
-  then errorlabstrm "New Morphism"
-    (str "The term " ++ prterm m ++ str " is already declared as a morpism")
-  else 
-    let env = Global.env() in
-    let mext = (current_constant lem_name) in
-    let typeofm = (Typing.type_of env Evd.empty m) in
-    let typ = (nf_betaiota typeofm) in
-    let (argsrev, body) = (decompose_prod typ) in
-    let args = List.rev argsrev in
-    let args_t = (List.map snd args) in
-    let poss = (List.map setoid_table_mem args_t) in
-    let _ = assert (poss=profil) in
-      (if (eq_constr body mkProp)
-       then
-	 (let lem_2 = gen_lem_iff env m mext args_t poss 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
+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;
-				   profil = poss;
-				   arg_types = args_t;
+                                   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;
-				profil = poss;
-				arg_types = args_t;
-				lem2 = None}))));
+    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")   
+
 let morphism_hook stre ref =
   let pf_id = id_of_global ref in
   if (is_edited pf_id)
@@ -528,117 +646,199 @@ let new_named_morphism id m = new_morphism (constr_of m) id morphism_hook
 (****************************** The tactic itself *******************************)
 
 type constr_with_marks =
-  | MApp of constr_with_marks array 
-  | Toreplace
+  | MApp of morphism_class Lazy.t * constr_with_marks array 
+  | Toreplace of setoid
   | Tokeep
   | Mimp of constr_with_marks * constr_with_marks
 
 let is_to_replace = function
-  | Tokeep -> false
-  | Toreplace -> true
-  | MApp _ -> true
-  | Mimp _ -> true
+ | Tokeep -> false
+ | Toreplace _ -> true
+ | MApp _ -> true
+ | Mimp _ -> true
 
 let get_mark a = 
   Array.fold_left (||) false (Array.map is_to_replace a)
 
-let rec mark_occur t in_c =
-  if (eq_constr t in_c) then Toreplace else
+exception Use_replace
+
+let mark_occur gl hyp =
+ 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 -> assert false
+   in
+    Toreplace sa
+  else
     match kind_of_term in_c with
       | App (c,al) -> 
-	  let a = Array.map (mark_occur t) al
-	  in if (get_mark a) then (MApp a) else Tokeep
+	  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
       | Prod (_, c1, c2) -> 
 	  if (dependent (mkRel 1) c2)
 	  then Tokeep
 	  else 
-	    let c1m = mark_occur t c1 in
-	    let c2m = mark_occur t c2 in
+	    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
+ in aux
 
-let create_args ca ma bl c1 c2 = 
+let create_args ca ma args c1 c2 = 
   let rec aux i = function
     | [] -> []
-    | true::q -> 
-	if (is_to_replace ma.(i)) 
-	then (replace_term c1 c2 ca.(i))::ca.(i)::(aux (i+1) q)
-	else ca.(i)::ca.(i)::(aux (i+1) q)
-    | false::q -> ca.(i)::(aux (i+1) q)
+    | (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 bl
-
+    aux 0 args
 
-let res_tac c a hyp =
-  let sa = setoid_table_find a in
+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) in
+	   Auto.full_trivial)
+  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 a = 
-  let sa = setoid_table_find a in
-    (tclTRY (apply (mkApp ((Lazy.force coq_seq_refl), [|sa.set_a; sa.set_aeq; sa.set_th; c|]))))
+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;;
 
-let rec create_tac_list i a al c1 c2 hyp args_t = function
+(* 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 *)
+       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
   | [] -> []
-  | false::q -> create_tac_list (i+1) a al c1 c2 hyp args_t q
-  | true::q -> 
+  | (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 false al.(i) a.(i) c1 c2 hyp)::(create_tac_list (i+1) a al c1 c2 hyp args_t q)
-      else (id_res_tac al.(i) (List.nth args_t i))::(create_tac_list (i+1) a al c1 c2 hyp args_t q)
-(*      else tclIDTAC::(create_tac_list (i+1) a al c1 c2 hyp q) *)
-
-and zapply is_r gl gl_m c1 c2 hyp glll = (match ((kind_of_term gl), gl_m) with
-  | ((App (c,al)),(MApp a)) -> (
-      try 
-	let m = morphism_table_find c in
-	let args = Array.of_list (create_args al a m.profil c1 c2) in
-	  if is_r
-	  then tclTHENS (apply (mkApp (m.lem, args)))
-	    ((create_tac_list 0 a al c1 c2 hyp m.arg_types m.profil)@[tclIDTAC])
- 	  else (match m.lem2 with
-		  | None -> 
-		      tclTHENS (apply (mkApp (m.lem, args))) (create_tac_list 0 a al c1 c2 hyp m.arg_types m.profil)
-		  | Some xom -> 
-		      tclTHENS (apply (mkApp (xom, args))) (create_tac_list 0 a al c1 c2 hyp m.arg_types m.profil))
-      with Not_found -> errorlabstrm "Setoid_replace" 
-	  (str "The term " ++ prterm c ++ str " has not been declared as a morphism"))
+      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 m = morphism_table_find fleche_constr in
-	  let args = Array.of_list (create_args al a m.profil c1 c2) in  
+	  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.arg_types m.profil)@[unfold_constr (ConstRef fleche_cp)]))
-(*		 ((create_tac_list 0 a al c1 c2 hyp m.arg_types m.profil)@[tclIDTAC])) *)
-	else (zapply is_r new_concl (MApp a) c1 c2 hyp)
-(*      let args = Array.of_list (create_args [|hh; cc|] [|hhm; ccm|] [true;true] c1 c2) in
-	if is_r
-	then tclTHENS (apply (mkApp ((Lazy.force coq_fleche_ext), args)))
-	  ((create_tac_list 0 [|hhm; ccm|] [|hh; cc|] c1 c2 hyp [mkProp; mkProp] [true;true])@[tclIDTAC])
-	else tclTHENS (apply (mkApp ((Lazy.force coq_fleche_ext2), args)))
-	  ((create_tac_list 0 [|hhm; ccm|] [|hh; cc|] c1 c2 hyp [mkProp; mkProp] [true;true])@[tclIDTAC])
-*)
-  | (_, Toreplace) -> 
+		 ((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"
@@ -657,17 +857,20 @@ and zapply is_r gl gl_m c1 c2 hyp glll = (match ((kind_of_term gl), gl_m) with
 		    else 
 		      apply (mkApp (Lazy.force coqproj1,[|(mkArrow hc1 hc2);(mkArrow hc2 hc1);h|]))
 	   )
-      else (res_tac gl (pf_type_of glll gl) hyp) (* tclORELSE Auto.full_trivial tclIDTAC *)
+      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"))
-  | _ -> anomaly ("Bug in Setoid_replace")) glll
+  | _ -> assert false) glll
 
 let setoid_replace c1 c2 hyp gl =
   let but = (pf_concl gl) in
-    (zapply true but (mark_occur c1 but) c1 c2 hyp) gl
+   try
+    (zapply None true but (mark_occur gl hyp c1 but) c1 c2 hyp) gl
+   with
+    Use_replace -> (!replace c1 c2) gl
 
 let general_s_rewrite lft2rgt c gl =
   let ctype = pf_type_of gl c in
@@ -681,6 +884,8 @@ let general_s_rewrite lft2rgt c gl =
     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 setoid_rewriteLR = general_s_rewrite true
 
 let setoid_rewriteRL = general_s_rewrite false
diff --git a/tactics/setoid_replace.mli b/tactics/setoid_replace.mli
index 059a25010..02046c55b 100644
--- a/tactics/setoid_replace.mli
+++ b/tactics/setoid_replace.mli
@@ -12,9 +12,14 @@ open Term
 open Proof_type
 open Topconstr
 
+
+val register_replace : (constr -> constr -> tactic) -> unit
+
+val print_setoids : unit -> unit
+
 val equiv_list : unit -> constr list
 
-val setoid_replace : constr -> constr -> constr option -> tactic
+val setoid_replace : constr -> constr -> tactic
 
 val setoid_rewriteLR : constr -> tactic