New algorithm to resolve morphisms, after discussion with Nicolas

Tabareau: 
- first pass: generation of the Morphism constraints with metavariables
  for unspecified relations by one fold over the term. 
  This builds a "respect" proof term for the whole term with holes.
- second pass: constraint solving of the evars, taking care of finding a
  solution for all the evars at once. 
- third step: normalize proof term by found evars, apply it, done!
Works with any relation, currently not as efficient as it could be due
to bad handling of evars. Also needs some fine tuning of the instances
declared in Morphisms.v that are used during proof search, e.g. using
priorities.

Reorganize Classes.* accordingly, separating the setoids in
Classes.SetoidClass from the general morphisms in Classes.Morphisms
and the generally applicable relation theory in Classes.Relations.


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

13 files changed, 570 insertions, 413 deletions

diff --git a/Makefile.common b/Makefile.common
index 3ba5fcede..c0537f264 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -704,8 +704,8 @@ SETOIDSVO:= theories/Setoids/Setoid_tac.vo theories/Setoids/Setoid_Prop.vo theor
 
 UNICODEVO:= theories/Unicode/Utf8.vo
 
-CLASSESVO:= theories/Classes/Init.vo theories/Classes/Relations.vo theories/Classes/SetoidClass.vo \
-	 theories/Classes/SetoidTactics.vo theories/Classes/SetoidDec.vo
+CLASSESVO:= theories/Classes/Init.vo theories/Classes/Relations.vo theories/Classes/Morphisms.vo \
+	 theories/Classes/SetoidClass.vo theories/Classes/SetoidTactics.vo theories/Classes/SetoidDec.vo
 
 THEORIESVO:=\
   $(INITVO) $(LOGICVO) $(ARITHVO) $(BOOLVO) $(NARITHVO) $(ZARITHVO) \
diff --git a/contrib/subtac/g_subtac.ml4 b/contrib/subtac/g_subtac.ml4
index 51e1a1709..337cd1696 100644
--- a/contrib/subtac/g_subtac.ml4
+++ b/contrib/subtac/g_subtac.ml4
@@ -140,7 +140,7 @@ VERNAC COMMAND EXTEND Subtac_Admit_Obligations
 
 VERNAC COMMAND EXTEND Subtac_Set_Solver
 | [ "Obligations" "Tactic" ":=" tactic(t) ] -> [ 
-    Subtac.require_library "Coq.Program.Tactics";
+    Coqlib.check_required_library ["Coq";"Program";"Tactics"];
     Tacinterp.add_tacdef false [((dummy_loc, id_of_string "obligations_tactic"), true, t)] ]
 END
 
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index febfb0494..f9ab283ad 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -216,6 +216,7 @@ let instances r =
     with Not_found -> unbound_class (Global.env()) (loc_of_reference r, id)
 
 let solve_instanciation_problem = ref (fun _ _ _ _ -> assert false)
+let solve_instanciations_problem = ref (fun _ _ -> assert false)
 
 let resolve_typeclass env ev evi (evd, defined as acc) =
   try
@@ -250,7 +251,7 @@ let resolve_one_typeclass_evd env evd types =
 	let evm' = Evd.evars_of evd' in
 	  match Evd.evar_body (Evd.find evm' ev) with
 	      Evar_empty -> raise Not_found
-	    | Evar_defined c -> c
+	    | Evar_defined c -> Evarutil.nf_evar evm' c
       else raise Not_found
   with Exit -> raise Not_found
 
@@ -278,6 +279,8 @@ let destClassApp c =
     | _ -> None
 
 let resolve_typeclasses ?(check=true) env sigma evd =
+(*   try !solve_instanciations_problem env (Evarutil.nf_evar_defs evd) *)
+(*   with _ -> *)
   let evm = Evd.evars_of evd in
   let tc_evars = 
     let f ev evi acc =
@@ -296,14 +299,14 @@ let resolve_typeclasses ?(check=true) env sigma evd =
 	(fun ev evi acc -> 
 	  if (Evd.mem tc_evars ev || not (Evd.mem evm ev)) && evi.evar_body = Evar_empty then
 	    resolve_typeclass env ev evi acc 
-	  else acc) 
+	  else acc)
 	(Evd.evars_of evars) (evars, false) 
     in
       if not progress then evars'
       else
 	sat (Evarutil.nf_evar_defs evars')
-  in sat evd
-
+  in sat (Evarutil.nf_evar_defs evd)
+  
 let class_of_constr c = 
   let extract_ind c =
     match kind_of_term c with
diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli
index ec3350a58..db408c889 100644
--- a/pretyping/typeclasses.mli
+++ b/pretyping/typeclasses.mli
@@ -64,6 +64,7 @@ val resolve_typeclass : env -> evar -> evar_info -> evar_defs * bool -> evar_def
 val resolve_typeclasses : ?check:bool -> env -> evar_map -> evar_defs -> evar_defs
 
 val solve_instanciation_problem : (env -> evar_defs -> existential_key -> evar_info -> evar_defs * bool) ref
+val solve_instanciations_problem : (env -> evar_defs -> evar_defs) ref
 
 type substitution = (identifier * constr) list
 
diff --git a/tactics/class_setoid.ml4 b/tactics/class_setoid.ml4
index dcc3ffbd2..b0a6b36c6 100644
--- a/tactics/class_setoid.ml4
+++ b/tactics/class_setoid.ml4
@@ -54,6 +54,7 @@ let coq_proj2 = lazy(gen_constant ["Init"; "Logic"] "proj2")
 let iff = lazy (gen_constant ["Init"; "Logic"] "iff")
 let impl = lazy (gen_constant ["Program"; "Basics"] "impl")
 let arrow = lazy (gen_constant ["Program"; "Basics"] "arrow")
+let coq_id = lazy (gen_constant ["Program"; "Basics"] "id")
 
 let reflexive_type = lazy (gen_constant ["Classes"; "Relations"] "Reflexive")
 let reflexive_proof = lazy (gen_constant ["Classes"; "Relations"] "reflexive")
@@ -66,8 +67,8 @@ let transitive_proof = lazy (gen_constant ["Classes"; "Relations"] "transitive")
 
 let inverse = lazy (gen_constant ["Classes"; "Relations"] "inverse")
 
-let respectful_dep = lazy (gen_constant ["Classes"; "Relations"] "respectful_dep")
-let respectful = lazy (gen_constant ["Classes"; "Relations"] "respectful")
+let respectful_dep = lazy (gen_constant ["Classes"; "Morphisms"] "respectful_dep")
+let respectful = lazy (gen_constant ["Classes"; "Morphisms"] "respectful")
 
 let iff_equiv = lazy (gen_constant ["Classes"; "Relations"] "iff_equivalence")
 let eq_equiv = lazy (gen_constant ["Classes"; "SetoidClass"] "eq_equivalence")
@@ -100,7 +101,7 @@ exception Found of (constr * constr * (types * types) list * constr * constr arr
 
 let resolve_morphism_evd env evd app = 
   let ev = Evarutil.e_new_evar evd env app in
-  let evd' = resolve_typeclasses ~check:false env (Evd.evars_of !evd) !evd in
+  let evd' = resolve_typeclasses ~check:true env (Evd.evars_of !evd) !evd in
   let evm' = Evd.evars_of evd' in
     match Evd.evar_body (Evd.find evm' (fst (destEvar ev))) with
 	Evd.Evar_empty -> raise Not_found
@@ -141,17 +142,18 @@ let build_signature isevars env m cstrs finalcstr =
       | _, _ -> assert false
   in aux m cstrs
 
-let reflexivity_proof env carrier relation x =
-  let goal = 
+let reflexivity_proof env evars carrier relation x =
+  let goal =
     mkApp (Lazy.force reflexive_type, [| carrier ; relation |])
   in
-    try let inst = resolve_one_typeclass env goal in
-	  mkApp (Lazy.force reflexive_proof, [| carrier ; relation ; inst ; x |])
-    with Not_found ->
-      let meta = Evarutil.new_meta() in
-	mkCast (mkMeta meta, DEFAULTcast, mkApp (relation, [| x; x |]))
+  let inst = Evarutil.e_new_evar evars env goal in
+    (* try resolve_one_typeclass env goal *)
+  mkApp (Lazy.force reflexive_proof, [| carrier ; relation ; inst ; x |])
+    (*     with Not_found -> *)
+(*       let meta = Evarutil.new_meta() in *)
+(* 	mkCast (mkMeta meta, DEFAULTcast, mkApp (relation, [| x; x |])) *)
 	  
-let resolve_morphism env sigma direction oldt m args args' cstr = 
+let resolve_morphism env sigma oldt m args args' cstr evars =
   let (morphism_cl, morphism_proj) = Lazy.force morphism_class in
   let morph_instance, proj, sigargs, m', args, args' = 
 (*     if is_equiv env sigma m then  *)
@@ -165,45 +167,38 @@ let resolve_morphism env sigma direction oldt m args args' cstr =
 (*       let m' = mkApp (m, [| a; r; s |]) in *)
 (* 	inst, proj, ctxargs, m', rest, rest' *)
 (*     else *)
-    let evars = ref (Evd.create_evar_defs Evd.empty) in
-    let pars =
-	match Array.length args with
-	    1 -> [1]
-	  | 2 -> [2;1]
-	  | 3 -> [3;2;1]
-	  | _ -> [4;3;2;1]
-      in
-	try 
-	  List.iter (fun n ->
-	    evars := Evd.create_evar_defs Evd.empty;
-	    let morphargs, morphobjs = array_chop (Array.length args - n) args in
-	    let morphargs', morphobjs' = array_chop (Array.length args - n) args' in
-	    let appm = mkApp(m, morphargs) in
-	    let appmtype = Typing.type_of env sigma appm in
-	    let signature, sigargs = build_signature evars env appmtype (Array.to_list morphobjs') cstr in
-	    let cl_args = [| appmtype ; signature ; appm |] in
-	    let app = mkApp (mkInd morphism_cl.cl_impl, cl_args) in
-	      try 
-		let morph = resolve_morphism_evd env evars app in
-		let evm = Evd.evars_of !evars in
-		let sigargs = List.map 
-		  (fun x, y -> Reductionops.nf_evar evm x, Reductionops.nf_evar evm y) 
-		  sigargs 
-		in
-		let appm = Reductionops.nf_evar evm appm in
-		let cl_args = Array.map (Reductionops.nf_evar evm) cl_args in
-		let proj = 
-		  mkApp (mkConst morphism_proj, 
-			Array.append cl_args [|morph|])
-		in
-		  raise (Found (morph, proj, sigargs, appm, morphobjs, morphobjs'))
-	      with Not_found -> ()
-		| Reduction.NotConvertible -> ()
-		| Stdpp.Exc_located (_, Pretype_errors.PretypeError _) 
-		| Pretype_errors.PretypeError _ -> ())
-	    pars;
-	  raise Not_found
-	with Found x -> x
+    let first = 
+      let first = ref (-1) in
+	for i = 0 to Array.length args' - 1 do
+	  if !first = -1 && args'.(i) <> None then first := i
+	done;
+	!first
+    in
+(*       try  *)
+	let morphargs, morphobjs = array_chop first args in
+	let morphargs', morphobjs' = array_chop first args' in
+	let appm = mkApp(m, morphargs) in
+	let appmtype = Typing.type_of env sigma appm in
+	let signature, sigargs = build_signature evars env appmtype (Array.to_list morphobjs') cstr in
+	let cl_args = [| appmtype ; signature ; appm |] in
+	let app = mkApp (mkInd morphism_cl.cl_impl, cl_args) in
+(* 	let morph = resolve_morphism_evd env evars app in *)
+	let morph = Evarutil.e_new_evar evars env app in
+(* 	let evm = Evd.evars_of !evars in *)
+(* 	let sigargs = List.map  *)
+(* 	  (fun x, y -> Reductionops.nf_evar evm x, Reductionops.nf_evar evm y)  *)
+(* 	  sigargs  *)
+(* 	in *)
+(* 	let appm = Reductionops.nf_evar evm appm in *)
+(* 	let cl_args = Array.map (Reductionops.nf_evar evm) cl_args in *)
+	let proj = 
+	  mkApp (mkConst morphism_proj, 
+		Array.append cl_args [|morph|])
+	in
+	  morph, proj, sigargs, appm, morphobjs, morphobjs'
+(*       with Reduction.NotConvertible *)
+(* 	| Stdpp.Exc_located (_, Pretype_errors.PretypeError _)  *)
+(* 	| Pretype_errors.PretypeError _ -> raise Not_found *)
   in 
   let projargs, respars, typeargs = 
     array_fold_left2 
@@ -211,7 +206,7 @@ let resolve_morphism env sigma direction oldt m args args' cstr =
 	let (carrier, relation), sigargs = split_head sigargs in
 	  match y with
 	      None ->
-		let refl_proof = reflexivity_proof env carrier relation x in
+		let refl_proof = reflexivity_proof env evars carrier relation x in
 		  [ refl_proof ; x ; x ] @ acc, sigargs, x :: typeargs'
 	    | Some (p, (_, _, _, t')) ->
 		[ p ; t'; x ] @ acc, sigargs, t' :: typeargs')
@@ -223,13 +218,24 @@ let resolve_morphism env sigma direction oldt m args args' cstr =
 	[ a, r ] -> (proof, (a, r, oldt, newt))
       | _ -> assert(false)
 
-let build_new gl env sigma direction occs origt newt hyp hypinfo concl cstr =
+let build_new gl env sigma occs origt newt hyp hypinfo concl cstr evars =
   let is_occ occ = occs = [] || List.mem occ occs in
   let rec aux t occ cstr =
     match kind_of_term t with
       | _ when eq_constr t origt -> 
 	  if is_occ occ then
-	    Some (hyp, hypinfo), succ occ
+	    match cstr with
+		None -> Some (hyp, hypinfo), succ occ
+	      | Some _ ->
+		  let (car, r, orig, dest) = hypinfo in
+		  let res = 
+		    try 
+		      Some (resolve_morphism env sigma t 
+			       (mkLambda (Name (id_of_string "x"), car, mkRel 1))
+			       (* (mkApp (Lazy.force coq_id, [| car |])) *)
+			       [| origt |] [| Some (hyp, hypinfo) |] cstr evars)
+		    with Not_found -> None
+		  in res, succ occ
 	  else None, succ occ
 
       | App (m, args) ->
@@ -242,7 +248,7 @@ let build_new gl env sigma direction occs origt newt hyp hypinfo concl cstr =
 	    if List.for_all (fun x -> x = None) args' then None
 	    else 
 	      let args' = Array.of_list (List.rev args') in
-		(try Some (resolve_morphism env sigma direction t m args args' cstr)
+		(try Some (resolve_morphism env sigma t m args args' cstr evars)
 		  with Not_found -> None)
 	  in res, occ
 
@@ -252,9 +258,9 @@ let build_new gl env sigma direction occs origt newt hyp hypinfo concl cstr =
 	  let res = 
 	    if x' = None && b' = None then None
 	    else 
-	      (try Some (resolve_morphism env sigma direction t
+	      (try Some (resolve_morphism env sigma t
 			    (arrow_morphism (pf_type_of gl x) (pf_type_of gl b)) [| x ; b |] [| x' ; b' |]
-			    cstr)
+			    cstr evars)
 		with Not_found -> None)
 	  in res, occ
 
@@ -287,6 +293,13 @@ let decompose_setoid_eqhyp gl env sigma c left2right t =
     if left2right then res
     else (c, (car, mkApp (Lazy.force inverse, [| car ; rel |]), y, x))
 
+let resolve_all_typeclasses env evd = 
+  Eauto.resolve_all_evars env (fun x -> Typeclasses.class_of_constr x <> None) evd
+    
+(* let _ =  *)
+(*   Typeclasses.solve_instanciation_problem := *)
+(*     (fun env evd ev evi -> resolve_all_typeclasses env evd, true) *)
+
 let cl_rewrite_clause c left2right occs clause gl =
   let env = pf_env gl in
   let sigma = project gl in
@@ -302,10 +315,19 @@ let cl_rewrite_clause c left2right occs clause gl =
 	None -> (mkProp, mkApp (Lazy.force inverse, [| mkProp; Lazy.force impl |]))
       | Some _ -> (mkProp, Lazy.force impl)
   in
-  let eq, _ = build_new gl env sigma left2right occs origt newt hypt hypinfo concl (Some cstr) in
+  let evars = ref (Evd.create_evar_defs Evd.empty) in
+  let eq, _ = build_new gl env sigma occs origt newt hypt hypinfo concl (Some cstr) evars in
     match eq with  
 	Some (p, (_, _, oldt, newt)) -> 
-	  (match is_hyp with
+(* 	  evars := Typeclasses.resolve_typeclasses ~check:false env (Evd.evars_of !evars) !evars; *)
+	  evars := Classes.resolve_all_typeclasses env !evars;
+(* 	  evars := resolve_all_typeclasses env !evars; *)
+	  evars := Evarutil.nf_evar_defs !evars;
+	  let p = Evarutil.nf_isevar !evars p in
+	  let newt = Evarutil.nf_isevar !evars newt in
+	  let undef = Evd.undefined_evars !evars in
+	    tclTHEN (Refiner.tclEVARS (Evd.evars_of undef))
+	      (match is_hyp with
 	    | Some id -> Tactics.apply_in true id [p,NoBindings]
 	    | None -> 
 		let meta = Evarutil.new_meta() in
diff --git a/theories/Classes/Init.v b/theories/Classes/Init.v
index b5352e720..aec260873 100644
--- a/theories/Classes/Init.v
+++ b/theories/Classes/Init.v
@@ -1 +1 @@
-Ltac typeclass_instantiation := eauto 50 with typeclass_instances || eauto.
+Ltac typeclass_instantiation := eauto with typeclass_instances || eauto.
diff --git a/theories/Classes/Morphisms.v b/theories/Classes/Morphisms.v
new file mode 100644
index 000000000..09a58fa01
--- /dev/null
+++ b/theories/Classes/Morphisms.v
@@ -0,0 +1,350 @@
+(* -*- coq-prog-args: ("-emacs-U" "-nois") -*- *)
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(* Typeclass-based morphisms with standard instances for equivalence relations.
+ 
+   Author: Matthieu Sozeau
+   Institution: LRI, CNRS UMR 8623 - UniversitĂcopyright Paris Sud
+   91405 Orsay, France *)
+
+(* $Id: FSetAVL_prog.v 616 2007-08-08 12:28:10Z msozeau $ *)
+
+Require Import Coq.Program.Program.
+Require Import Coq.Classes.Init.
+Require Export Coq.Classes.Relations.
+
+Set Implicit Arguments.
+Unset Strict Implicit.
+
+(** * Morphisms.
+
+   We now turn to the definition of [Morphism] and declare standard instances. 
+   These will be used by the [clrewrite] tactic later. *)
+
+(** Respectful morphisms. *)
+
+Definition respectful_depT (A : Type) (R : relationT A) 
+  (B : A -> Type) (R' : forall x y, B x -> B y -> Type) : relationT (forall x : A, B x) := 
+  fun f g => forall x y : A, R x y -> R' x y (f x) (g y).
+
+Definition respectfulT A (eqa : relationT A) B (eqb : relationT B) : relationT (A -> B) :=
+  Eval compute in (respectful_depT eqa (fun _ _ => eqb)).
+
+Definition respectful A (R : relation A) B (R' : relation B) : relation (A -> B) :=
+  fun f g => forall x y : A, R x y -> R' (f x) (g y).
+
+(** Notations reminiscent of the old syntax for declaring morphisms.
+   We use three + or - for type morphisms, and two for [Prop] ones.
+   *)
+
+Notation " R +++> R' " := (@respectfulT _ R _ R') (right associativity, at level 20).
+Notation " R ---> R' " := (@respectfulT _ (flip R) _ R') (right associativity, at level 20).
+
+Notation " R ++> R' " := (@respectful _ R _ R') (right associativity, at level 20).
+Notation " R --> R' " := (@respectful _ (inverse R) _ R') (right associativity, at level 20).
+
+(** A morphism on a relation [R] is an object respecting the relation (in its kernel). 
+   The relation [R] will be instantiated by [respectful] and [A] by an arrow type 
+   for usual morphisms. *)
+
+Class Morphism A (R : relationT A) (m : A) :=
+  respect : R m m.
+
+(** Here we build an equivalence instance for functions which relates respectful ones only. *)
+
+Definition respecting [ Equivalence A (R : relation A), Equivalence B (R' : relation B) ] : Type := 
+  { morph : A -> B | respectful R R' morph morph }.
+
+Ltac obligations_tactic ::= program_simpl.
+
+Program Instance [ Equivalence A (R : relation A), Equivalence B (R' : relation B) ] => 
+  respecting_equiv : Equivalence respecting
+  (fun (f g : respecting) => forall (x y : A), R x y -> R' (`f x) (`g y)).
+
+  Next Obligation.
+  Proof.
+    constructor ; intros.
+    destruct x ; simpl.
+    apply r ; auto.
+  Qed.
+
+  Next Obligation.
+  Proof.
+    constructor ; intros.
+    sym ; apply H.
+    sym ; auto.
+  Qed.
+
+  Next Obligation.
+  Proof.
+    constructor ; intros.
+    trans ((`y) y0).
+    apply H ; auto.
+    apply H0. refl.
+  Qed.
+
+(** Can't use the definition [notT] as it gives a universe inconsistency. *)
+
+Ltac obligations_tactic ::= program_simpl ; simpl_relation.
+
+Program Instance notT_arrow_morphism : 
+  Morphism (Type -> Type) (arrow ---> arrow) (fun X : Type => X -> False).
+
+Program Instance not_iso_morphism : 
+  Morphism (Type -> Type) (iso +++> iso) (fun X : Type => X -> False).
+
+Program Instance not_impl_morphism :
+  Morphism (Prop -> Prop) (impl --> impl) not.
+
+Program Instance not_iff_morphism : 
+  Morphism (Prop -> Prop) (iff ++> iff) not.
+
+(** We make the type implicit, it can be infered from the relations. *)
+
+Implicit Arguments Morphism [A].
+
+(** Leibniz *)
+
+Program Definition eq_morphism A : Morphism (eq ++> eq ++> iff) (eq (A:=A)).
+Proof. intros ; constructor ; intros.
+  obligations_tactic.
+  subst.
+  intuition.
+Qed.
+
+(* Program Definition arrow_morphism `A B` (m : A -> B) : Morphism (eq ++> eq) m. *)
+
+(** Any binary morphism respecting some relations up to [iff] respects 
+   them up to [impl] in each way. Very important instances as we need [impl]
+   morphisms at the top level when we rewrite. *)
+
+Program Instance `A` (R : relation A) `B` (R' : relation B)
+  [ ? Morphism (R ++> R' ++> iff) m ] =>
+
+  iff_impl_binary_morphism : ? Morphism (R ++> R' ++> impl) m.
+
+  Next Obligation.
+  Proof.
+    destruct respect with x y x0 y0 ; auto.
+  Qed.
+
+Program Instance `A` (R : relation A) `B` (R' : relation B)
+  [ ? Morphism (R ++> R' ++> iff) m ] =>
+  iff_inverse_impl_binary_morphism : ? Morphism (R ++> R' ++> inverse impl) m.
+
+  Next Obligation.
+  Proof.
+    destruct respect with x y x0 y0 ; auto.
+  Qed.
+
+(** The complement of a relation conserves its morphisms. *)
+
+Program Instance `A` (RA : relation A) [ ? Morphism (RA ++> RA ++> iff) R ] => 
+  complement_morphism : ? Morphism (RA ++> RA ++> iff) (complement R).
+
+  Next Obligation.
+  Proof.
+    unfold complement ; intros.
+    pose (respect).
+    pose (r x y H).
+    pose (r0 x0 y0 H0).
+    intuition.
+  Qed.
+
+(** The inverse too. *)
+
+Program Instance `A` (RA : relation A) [ ? Morphism (RA ++> RA ++> iff) R ] => 
+  inverse_morphism : ? Morphism (RA ++> RA ++> iff) (inverse R).
+
+  Next Obligation.
+  Proof.
+    unfold inverse ; unfold flip.
+    apply respect ; auto.
+  Qed.
+
+(* Definition respectful' A (R : relation A) B (R' : relation B) (f : A -> B) : relation A := *)
+(*   fun x y => R x y -> R' (f x) (f y). *)
+
+(* Definition morphism_respectful' A (R : relation A) B (R' : relation B) (f : A -> B) *)
+(*   [ ? Morphism (R ++> R') f ] (x y : A) : respectful' R R' f x y. *)
+(* intros. *)
+(* destruct H. *)
+(* red in respect0. *)
+(* red.  *)
+(* apply respect0. *)
+(* Qed. *)
+
+(* Existing Instance morphism_respectful'. *)
+
+(* Goal forall A [ Equivalence A (eqA : relation A) ] (R : relation A) [ ? Morphism (eqA ++> iff) m ] (x y : A)  *)
+(*   [ ? Morphism (eqA ++> eqA) m' ] (m' : A -> A), eqA x y -> True. *)
+(*   intros. *)
+(*   cut (relation A) ; intros R'. *)
+(*   cut ((eqA ++> R') m' m') ; intros. *)
+(*   assert({ R' : relation A & Reflexive R' }). *)
+(*   econstructor. *)
+(*   typeclass_instantiation. *)
+  
+
+(*   assert (exists R' : relation A, Morphism ((fun x y => eqA x y -> R' (m' x) (m' y)) ++> iff) m). *)
+(*   eapply ex_intro. *)
+(*   unfold respectful. *)
+(*   typeclass_instantiation. *)
+  
+
+(*   assert (exists R', Morphism (R' ++> iff) m /\ Morphism (eqA ++> R') m'). *)
+(*   typeclass_instantiation. *)
+(*   Set Printing All. *)
+(*   Show Proof. *)
+  
+  
+(*   apply respect. *)
+
+(** Partial applications are ok when a proof of refl is available. *)
+
+(** A proof of [R x x] is available. *)
+
+(* Program Instance (A : Type) (R : relation A) B (R' : relation B) *)
+(*   [ ? Morphism (R ++> R') m ] [ ? Morphism R x ] => *)
+(*   morphism_partial_app_morphism : ? Morphism R' (m x). *)
+
+(*   Next Obligation. *)
+(*   Proof with auto. *)
+(*     apply (respect (m:=m))... *)
+(*     apply respect. *)
+(*   Qed. *)
+
+
+(** Morpshism declarations for partial applications. *)
+
+Program Instance [ Transitive A (R : relation A) ] (x : A) =>
+  trans_contra_inv_impl_morphism : ? Morphism (R --> inverse impl) (R x).
+
+  Next Obligation.
+  Proof with auto.
+    trans y...
+  Qed.
+
+Program Instance [ Transitive A (R : relation A) ] (x : A) =>
+  trans_co_impl_morphism : ? Morphism (R ++> impl) (R x).
+
+  Next Obligation.
+  Proof with auto.
+    trans x0...
+  Qed.
+
+Program Instance [ Transitive A (R : relation A), Symmetric A R ] (x : A) =>
+  trans_sym_co_inv_impl_morphism : ? Morphism (R ++> inverse impl) (R x).
+
+  Next Obligation.
+  Proof with auto.
+    trans y...
+    sym...
+  Qed.
+
+Program Instance [ Transitive A (R : relation A), Symmetric A R ] (x : A) =>
+  trans_sym_contra_impl_morphism : ? Morphism (R --> impl) (R x).
+
+  Next Obligation.
+  Proof with auto.
+    trans x0...
+    sym...
+  Qed.
+
+Program Instance [ Equivalence A (R : relation A) ] (x : A) =>
+  equivalence_partial_app_morphism : ? Morphism (R ++> iff) (R x).
+
+  Next Obligation.
+  Proof with auto.
+    split. intros ; trans x0...
+    intros.
+    trans y...
+    sym...
+  Qed.
+
+(** With symmetric relations, variance is no issue ! *)
+
+Program Instance [ Symmetric A (R : relation A) ] B (R' : relation B) 
+  [ Morphism _ (R ++> R') m ] => 
+  sym_contra_morphism : ? Morphism (R --> R') m.
+
+  Next Obligation.
+  Proof with auto.
+    repeat (red ; intros). apply respect.
+    sym...
+  Qed.
+
+(** [R] is reflexive, hence we can build the needed proof. *)
+
+Program Instance [ Reflexive A (R : relation A) ] B (R' : relation B)
+  [ ? Morphism (R ++> R') m ] (x : A) =>
+  reflexive_partial_app_morphism : ? Morphism R' (m x).
+
+  Next Obligation.
+  Proof with auto.
+    intros.
+    apply (respect (m:=m))...
+    refl.
+  Qed.
+
+(** Every symmetric and transitive relation gives rise to an equivariant morphism. *)
+
+Program Instance [ Transitive A (R : relation A), Symmetric A R ] => 
+  trans_sym_morphism : ? Morphism (R ++> R ++> iff) R.
+
+  Next Obligation.
+  Proof with auto.
+    split ; intros.
+    trans x0... trans x... sym...
+  
+    trans y... trans y0... sym...
+  Qed.
+
+Program Instance [ Equivalence A (R : relation A) ] => 
+  equiv_morphism : ? Morphism (R ++> R ++> iff) R.
+
+  Next Obligation.
+  Proof with auto.
+    split ; intros.
+    trans x0... trans x... sym...
+  
+    trans y... trans y0... sym...
+  Qed.
+
+(** In case the rewrite happens at top level. *)
+
+Program Instance iff_inverse_impl_id : 
+  ? Morphism (iff ++> inverse impl) id.
+
+Program Instance inverse_iff_inverse_impl_id : 
+  ? Morphism (iff --> inverse impl) id.
+  
+Program Instance iff_impl_id : 
+  ? Morphism (iff ++> impl) id.
+
+Program Instance inverse_iff_impl_id : 
+  ? Morphism (iff --> impl) id.
+  
+(** Standard instances for [iff] and [impl]. *)
+
+(** Logical conjunction. *)
+
+(* Program Instance and_impl_iff_morphism : ? Morphism (impl ++> iff ++> impl) and. *)
+
+(* Program Instance and_iff_impl_morphism : ? Morphism (iff ++> impl ++> impl) and. *)
+
+Program Instance and_iff_morphism : ? Morphism (iff ++> iff ++> iff) and.
+
+(** Logical disjunction. *)
+
+(* Program Instance or_impl_iff_morphism : ? Morphism (impl ++> iff ++> impl) or. *)
+
+(* Program Instance or_iff_impl_morphism : ? Morphism (iff ++> impl ++> impl) or. *)
+
+Program Instance or_iff_morphism : ? Morphism (iff ++> iff ++> iff) or.
diff --git a/theories/Classes/Relations.v b/theories/Classes/Relations.v
index 6ecd4ac3c..694cab59b 100644
--- a/theories/Classes/Relations.v
+++ b/theories/Classes/Relations.v
@@ -7,11 +7,11 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* Typeclass-based setoids, tactics and standard instances.
-   TODO: explain clrewrite, clsubstitute and so on.
+(* Typeclass-based relations, tactics and standard instances.
+   This is the basic theory needed to formalize morphisms and setoids.
  
    Author: Matthieu Sozeau
-   Institution: LRI, CNRS UMR 8623 - UniversitÃcopyright Paris Sud
+   Institution: LRI, CNRS UMR 8623 - UniversitĂcopyright Paris Sud
    91405 Orsay, France *)
 
 (* $Id: FSetAVL_prog.v 616 2007-08-08 12:28:10Z msozeau $ *)
@@ -25,14 +25,14 @@ Unset Strict Implicit.
 Definition relationT A := A -> A -> Type.
 Definition relation A := A -> A -> Prop.
 
-Definition inverse A (R : relation A) : relation A := flip R.
+Definition inverse A (R : relation A) : relation A := fun x y => R y x.
 
 Lemma inverse_inverse : forall A (R : relation A), inverse (inverse R) = R.
 Proof. intros ; unfold inverse. apply (flip_flip R). Qed.
 
-Definition complementT A (R : relationT A) := fun x y => ! R x y.
+Definition complementT A (R : relationT A) := fun x y => notT (R x y).
 
-Definition complement A (R : relation A) := fun x y => ~ R x y.
+Definition complement A (R : relation A) := fun x y => R x y -> False.
 
 (** These are convertible. *)
 
@@ -112,7 +112,6 @@ Program Instance [ Reflexive A (R : relation A) ] =>
 
   Next Obligation. 
   Proof. 
-    unfold complement in * ; intros.
     apply H.
     apply reflexive.
   Qed.
@@ -122,7 +121,6 @@ Program Instance [ Irreflexive A (R : relation A) ] =>
 
   Next Obligation. 
   Proof. 
-    unfold complement in * ; intros.
     red ; intros.
     apply (irreflexive H).
   Qed.
@@ -131,12 +129,54 @@ Program Instance [ Symmetric A (R : relation A) ] => complement_symmetric : Symm
 
   Next Obligation.
   Proof.
-    unfold complement in *.
     red ; intros H'.
     apply (H (symmetric H')).
   Qed.
 
-(** Tactics to solve goals. Each tactic comes in two flavors:
+(** * Standard instances. *)
+
+Ltac simpl_relation :=
+  try red ; unfold inverse, flip, impl, arrow ; program_simpl ; try tauto ; 
+    repeat (red ; intros) ; try ( solve [ intuition ]).
+
+Ltac obligations_tactic ::= simpl_relation.
+
+(** The arrow is a reflexive and transitive relation on types. *)
+
+Program Instance arrow_refl : ? Reflexive arrow := 
+  reflexive X := id.
+
+Program Instance arrow_trans : ? Transitive arrow := 
+  transitive X Y Z f g := g o f.
+
+(** Isomorphism. *)
+
+Definition iso (A B : Type) := 
+  A -> B * B -> A.
+
+Program Instance iso_refl : ? Reflexive iso.
+Program Instance iso_sym : ? Symmetric iso.
+Program Instance iso_trans : ? Transitive iso.
+
+(** Logical implication. *)
+
+Program Instance impl_refl : ? Reflexive impl.
+Program Instance impl_trans : ? Transitive impl.
+
+(** Logical equivalence. *)
+
+Program Instance iff_refl : ? Reflexive iff.
+Program Instance iff_sym : ? Symmetric iff.
+Program Instance iff_trans : ? Transitive iff.
+
+(** Leibniz equality. *)
+
+Program Instance eq_refl : ? Reflexive (@eq A).
+Program Instance eq_sym : ? Symmetric (@eq A).
+Program Instance eq_trans : ? Transitive (@eq A).
+
+(** ** General tactics to solve goals on relations.
+   Each tactic comes in two flavors:
    - a tactic to immediately solve a goal without user intervention
    - a tactic taking input from the user to make progress on a goal *)
 
@@ -216,6 +256,9 @@ Ltac relation_trans :=
 
     | [ H : ?R ?A ?B ?C ?D ?X ?Y, H' : ?R ?A ?B ?C ?D ?Y ?Z |- ?R ?A ?B ?C ?D ?X ?Z ] => 
       apply (transitive (R:=R A B C D) (x:=X) (y:=Y) (z:=Z) H H')
+
+    | [ H : ?R ?A ?B ?C ?D ?E ?X ?Y, H' : ?R ?A ?B ?C ?D ?E ?Y ?Z |- ?R ?A ?B ?C ?D ?E ?X ?Z ] => 
+      apply (transitive (R:=R A B C D E) (x:=X) (y:=Y) (z:=Z) H H')
   end.
 
 Ltac relation_transitive Y := 
@@ -242,254 +285,13 @@ Ltac trans Y := relation_transitive Y.
 
 Ltac relation_tac := relation_refl || relation_sym || relation_trans.
 
-(** * Morphisms.
-
-   We now turn to the definition of [Morphism] and declare standard instances. 
-   These will be used by the [clrewrite] tactic later. *)
-
-(** Respectful morphisms. *)
-
-Definition respectful_depT (A : Type) (R : relationT A) 
-  (B : A -> Type) (R' : forall x y, B x -> B y -> Type) : relationT (forall x : A, B x) := 
-  fun f g => forall x y : A, R x y -> R' x y (f x) (g y).
-
-Definition respectfulT A (eqa : relationT A) B (eqb : relationT B) : relationT (A -> B) :=
-  Eval compute in (respectful_depT eqa (fun _ _ => eqb)).
-
-Definition respectful A (R : relation A) B (R' : relation B) : relation (A -> B) :=
-  fun f g => forall x y : A, R x y -> R' (f x) (g y).
-
-(** Notations reminiscent of the old syntax for declaring morphisms.
-   We use three + or - for type morphisms, and two for [Prop] ones.
-   *)
-
-Notation " R +++> R' " := (@respectfulT _ R _ R') (right associativity, at level 20).
-Notation " R ---> R' " := (@respectfulT _ (flip R) _ R') (right associativity, at level 20).
-
-Notation " R ++> R' " := (@respectful _ R _ R') (right associativity, at level 20).
-Notation " R --> R' " := (@respectful _ (inverse R) _ R') (right associativity, at level 20).
-
-(** A morphism on a relation [R] is an object respecting the relation (in its kernel). 
-   The relation [R] will be instantiated by [respectful] and [A] by an arrow type 
-   for usual morphisms. *)
-
-Class Morphism A (R : relationT A) (m : A) :=
-  respect : R m m.
-
-Ltac simpl_morphism :=
-  try red ; unfold inverse, flip, impl, arrow ; program_simpl ; try tauto ; 
-    try (red ; intros) ; try ( solve [ intuition ]).
-
-Ltac obligations_tactic ::= simpl_morphism.
-
-(** The arrow is a reflexive and transitive relation on types. *)
-
-Program Instance arrow_refl : ? Reflexive arrow := 
-  reflexive X := id.
-
-Program Instance arrow_trans : ? Transitive arrow := 
-  transitive X Y Z f g := g o f.
-
-(** Can't use the definition [notT] as it gives a to universe inconsistency. *)
-
-Program Instance notT_arrow_morphism : 
-  Morphism (Type -> Type) (arrow ---> arrow) (fun X : Type => X -> False).
-
-(** Isomorphism. *)
-
-Definition iso (A B : Type) := 
-  A -> B * B -> A.
-
-Program Instance iso_refl : ? Reflexive iso.
-Program Instance iso_sym : ? Symmetric iso.
-Program Instance iso_trans : ? Transitive iso.
-
-Program Instance not_iso_morphism : 
-  Morphism (Type -> Type) (iso +++> iso) (fun X : Type => X -> False).
-
-(** Logical implication. *)
-
-Program Instance impl_refl : ? Reflexive impl.
-Program Instance impl_trans : ? Transitive impl.
-
-Program Instance not_impl_morphism :
-  Morphism (Prop -> Prop) (impl --> impl) not.
-
-(** Logical equivalence. *)
-
-Program Instance iff_refl : ? Reflexive iff.
-Program Instance iff_sym : ? Symmetric iff.
-Program Instance iff_trans : ? Transitive iff.
-
-Program Instance not_iff_morphism : 
-  Morphism (Prop -> Prop) (iff ++> iff) not.
-
-(** We make the type implicit, it can be infered from the relations. *)
-
-Implicit Arguments Morphism [A].
-
-(** If you have a morphism from [RA] to [RB] you have a contravariant morphism 
-   from [RA] to [inverse RB]. *)
-
-Program Instance `A` (RA : relation A) `B` (RB : relation B) [ ? Morphism (RA ++> RB) m ] =>
-  morph_impl_co_contra_inverse :
-  ? Morphism (RA --> inverse RB) m.
-
-  Next Obligation.
-  Proof.
-    apply respect.
-    apply H.
-  Qed.
-
-(** Every transitive relation gives rise to a binary morphism on [impl], 
-   contravariant in the first argument, covariant in the second. *)
-
-Program Instance [ Transitive A (R : relation A) ] => 
-  trans_contra_co_morphism : ? Morphism (R --> R ++> impl) R.
-
-  Next Obligation.
-  Proof with auto.
-    trans x...
-    trans x0...
-  Qed.
-
-(** Dually... *)
-
-Program Instance [ Transitive A (R : relation A) ] =>
-  trans_co_contra_inv_impl_morphism : ? Morphism (R ++> R --> inverse impl) R.
-
-  Obligations Tactic := idtac.
-  
-  Next Obligation.
-  Proof with auto.
-    intros.
-    destruct (trans_contra_co_morphism (R:=inverse R)).
-    revert respect0.
-    unfold respectful, inverse, flip in * ; intros.
-    apply respect0 ; auto.
-  Qed.
-
-Obligations Tactic := simpl_morphism.
-
-(** With symmetric relations, variance is no issue ! *)
-
-Program Instance [ Symmetric A (R : relation A) ] B (R' : relation B) 
-  [ Morphism _ (R ++> R') m ] => 
-  sym_contra_morphism : ? Morphism (R --> R') m.
-
-  Next Obligation.
-  Proof with auto.
-    apply respect.
-    sym...
-  Qed.
-
-(** Every symmetric and transitive relation gives rise to an equivariant morphism. *)
-
-Program Instance [ Transitive A (R : relation A), Symmetric A R ] => 
-  trans_sym_morphism : ? Morphism (R ++> R ++> iff) R.
-
-  Next Obligation.
-  Proof with auto.
-    split ; intros.
-    trans x0... trans x... sym...
-  
-    trans y... trans y0... sym...
-  Qed.
-
-(** The complement of a relation conserves its morphisms. *)
-
-Program Instance `A` (RA : relation A) [ ? Morphism (RA ++> RA ++> iff) R ] => 
-  complement_morphism : ? Morphism (RA ++> RA ++> iff) (complement R).
-
-  Next Obligation.
-  Proof.
-    red ; unfold complement ; intros.
-    pose (respect).
-    pose (r x y H).
-    pose (r0 x0 y0 H0).
-    intuition.
-  Qed.
-
-(** The inverse too. *)
-
-Program Instance `A` (RA : relation A) [ ? Morphism (RA ++> RA ++> iff) R ] => 
-  inverse_morphism : ? Morphism (RA ++> RA ++> iff) (inverse R).
-
-  Next Obligation.
-  Proof.
-    unfold inverse ; unfold flip.
-    apply respect ; auto.
-  Qed.
-
-Program Instance [ Transitive A (R : relation A), Symmetric A R ] =>
-  trans_sym_contra_co_inv_impl_morphism : ? Morphism (R --> R ++> inverse impl) R.
-
-  Next Obligation.
-  Proof with auto.
-    trans y...
-    sym...
-    trans y0...
-    sym...
-  Qed.
-
-(** Any binary morphism respecting some relations up to [iff] respects 
-   them up to [impl] in each way. Very important instances as we need [impl]
-   morphisms at the top level when we rewrite. *)
-
-Program Instance `A` (R : relation A) `B` (R' : relation B) 
-  [ ? Morphism (R ++> R' ++> iff) m ] => 
-  iff_impl_binary_morphism : ? Morphism (R ++> R' ++> impl) m.
-
-  Next Obligation.
-  Proof.
-    destruct respect with x y x0 y0 ; auto.
-  Qed.
-
-Program Instance `A` (R : relation A) `B` (R' : relation B)
-  [ ? Morphism (R ++> R' ++> iff) m ] => 
-  iff_inverse_impl_binary_morphism : ? Morphism (R ++> R' ++> inverse impl) m.
-
-  Next Obligation.
-  Proof.
-    destruct respect with x y x0 y0 ; auto.
-  Qed.
-
-(** Standard instances for [iff] and [impl]. *)
-
-(** Logical conjunction. *)
-
-Program Instance and_impl_iff_morphism : ? Morphism (impl ++> iff ++> impl) and.
-
-Program Instance and_iff_impl_morphism : ? Morphism (iff ++> impl ++> impl) and.
-
-Program Instance and_iff_morphism : ? Morphism (iff ++> iff ++> iff) and.
-
-(** Logical disjunction. *)
-
-Program Instance or_impl_iff_morphism : ? Morphism (impl ++> iff ++> impl) or.
-
-Program Instance or_iff_impl_morphism : ? Morphism (iff ++> impl ++> impl) or.
-
-Program Instance or_iff_morphism : ? Morphism (iff ++> iff ++> iff) or.
-
-(** Leibniz equality. *)
-
-Program Instance eq_refl : ? Reflexive (@eq A).
-Program Instance eq_sym : ? Symmetric (@eq A).
-Program Instance eq_trans : ? Transitive (@eq A).
-
-Program Definition eq_morphism A : Morphism (eq ++> eq ++> iff) (eq (A:=A)) :=
-  trans_sym_morphism.
-
-Program Instance `A B` (m : A -> B) => arrow_morphism : ? Morphism (eq ++> eq) m.
-
 (** The [PER] typeclass. *)
 
 Class PER (carrier : Type) (pequiv : relationT carrier) :=
   per_sym :> Symmetric pequiv ;
   per_trans :> Transitive pequiv.
 
-(** We can build a PER on the coq function space if we have PERs on the domain and
+(** We can build a PER on the Coq function space if we have PERs on the domain and
    codomain. *)
 
 Program Instance [ PER A (R : relation A), PER B (R' : relation B) ] => 
@@ -520,38 +322,10 @@ Program Instance [ eq : Equivalence A eqA, ? Antisymmetric eq R ] =>
 
   Solve Obligations using unfold flip ; program_simpl ; eapply antisymmetric ; eauto.
 
-(** Here we build an equivalence instance for functions which relates respectful ones only. *)
-
-Definition respecting [ Equivalence A (R : relation A), Equivalence B (R' : relation B) ] : Type := 
-  { morph : A -> B | respectful R R' morph morph }.
-
-Ltac obligations_tactic ::= program_simpl.
-
-Program Instance [ Equivalence A (R : relation A), Equivalence B (R' : relation B) ] => 
-  respecting_equiv : Equivalence respecting
-  (fun (f g : respecting) => forall (x y : A), R x y -> R' (`f x) (`g y)).
+Program Instance [ eq : Equivalence A eqA, ? Antisymmetric eq (R : relation A) ] => 
+  inverse_antisymmetric : ? Antisymmetric eq (inverse R).
 
-  Next Obligation.
-  Proof.
-    constructor ; intros.
-    destruct x ; simpl.
-    apply r ; auto.
-  Qed.
-
-  Next Obligation.
-  Proof.
-    constructor ; intros.
-    sym ; apply H.
-    sym ; auto.
-  Qed.
-
-  Next Obligation.
-  Proof.
-    constructor ; intros.
-    trans ((`y) y0).
-    apply H ; auto.
-    apply H0. refl.
-  Qed.
+  Solve Obligations using unfold inverse, flip ; program_simpl ; eapply antisymmetric ; eauto.
 
 (** Leibinz equality [eq] is an equivalence relation. *)
 
diff --git a/theories/Classes/SetoidClass.v b/theories/Classes/SetoidClass.v
index 78e53aa01..5e18ef2af 100644
--- a/theories/Classes/SetoidClass.v
+++ b/theories/Classes/SetoidClass.v
@@ -23,6 +23,7 @@ Set Implicit Arguments.
 Unset Strict Implicit.
 
 Require Export Coq.Classes.Relations.
+Require Export Coq.Classes.Morphisms.
 
 (** A setoid wraps an equivalence. *)
 
@@ -30,6 +31,10 @@ Class Setoid A :=
   equiv : relation A ;
   setoid_equiv :> Equivalence A equiv.
 
+Program Instance [ eqa : Equivalence A (eqA : relation A) ] => 
+  equivalence_setoid : Setoid A :=
+  equiv := eqA ; setoid_equiv := eqa.
+
 (** Shortcuts to make proof search easier. *)
 
 Definition setoid_refl [ sa : Setoid A ] : Reflexive equiv.
@@ -43,8 +48,8 @@ Proof. eauto with typeclass_instances. Qed.
 
 (** Standard setoids. *)
 
-Program Instance eq_setoid : Setoid A :=
-  equiv := eq ; setoid_equiv := eq_equivalence.
+(* Program Instance eq_setoid : Setoid A := *)
+(*   equiv := eq ; setoid_equiv := eq_equivalence. *)
 
 Program Instance iff_setoid : Setoid Prop :=
   equiv := iff ; setoid_equiv := iff_equivalence.
@@ -56,14 +61,7 @@ Program Instance iff_setoid : Setoid Prop :=
 
 Notation " x == y " := (equiv x y) (at level 70, no associativity) : type_scope.
 
-Notation " x =/= y " := (~ x == y) (at level 70, no associativity) : type_scope.
-
-Lemma nequiv_sym : forall [ s : Setoid A ] (x y : A), x =/= y -> y =/= x.
-Proof with auto.
-  intros ; red ; intros.
-  apply H.
-  sym...
-Qed.
+Notation " x =/= y " := (complement equiv x y) (at level 70, no associativity) : type_scope.
 
 (** Use the [clsubstitute] command which substitutes an equality in every hypothesis. *)
 
@@ -82,15 +80,15 @@ Ltac clsubst_nofail :=
 
 Tactic Notation "clsubst" "*" := clsubst_nofail.
 
-Lemma nequiv_equiv : forall [ Setoid A ] (x y z : A), x =/= y -> y == z -> x =/= z.
-Proof.
-  intros; intro. 
+Lemma nequiv_equiv_trans : forall [ Setoid A ] (x y z : A), x =/= y -> y == z -> x =/= z.
+Proof with auto.
+  intros; intro.
   assert(z == y) by relation_sym.
   assert(x == y) by relation_trans.
   contradiction.
 Qed.
 
-Lemma equiv_nequiv : forall [ Setoid A ] (x y z : A), x == y -> y =/= z -> x =/= z.
+Lemma equiv_nequiv_trans : forall [ Setoid A ] (x y z : A), x == y -> y =/= z -> x =/= z.
 Proof.
   intros; intro. 
   assert(y == x) by relation_sym.
diff --git a/theories/Classes/SetoidTactics.v b/theories/Classes/SetoidTactics.v
index 39809865c..fb7f8827b 100644
--- a/theories/Classes/SetoidTactics.v
+++ b/theories/Classes/SetoidTactics.v
@@ -39,51 +39,3 @@ Ltac setoideq_ext :=
     [ |- @eq ?A ?X ?Y ] => apply (setoideq_eq (a:=A) X Y)
   end.
 
-Ltac setoid_tactic :=
-  match goal with
-    | [ H : ?eq ?x ?y |- ?eq ?y ?x ] => sym ; apply H
-    | [ |- ?eq ?x ?x ] => refl
-    | [ H : ?eq ?x ?y, H' : ?eq ?y ?z |- ?eq' ?x ?z ] => trans y ; [ apply H | apply H' ]
-    | [ H : ?eq ?x ?y, H' : ?eq ?z ?y |- ?eq' ?x ?z ] => trans y ; [ apply H | sym ; apply H' ]
-    | [ H : ?eq ?y ?x, H' : ?eq ?z ?y |- ?eq' ?x ?z ] => trans y ; [ sym ; apply H | sym ; apply H' ]
-    | [ H : ?eq ?y ?x, H' : ?eq ?y ?z |- ?eq' ?x ?z ] => trans y ; [ sym ; apply H | apply H' ]
-      
-    | [ H : ?eq ?x ?y |- @equiv _ _ _ ?y ?x ] => sym ; apply H
-    | [ |- @equiv _ _ _ ?x ?x ] => refl
-    | [ H : ?eq ?x ?y, H' : ?eq ?y ?z |- @equiv _ _ _ ?x ?z ] => trans y ; [ apply H | apply H' ]
-    | [ H : ?eq ?x ?y, H' : ?eq ?z ?y |- @equiv _ _ _ ?x ?z ] => trans y ; [ apply H | sym ; apply H' ]
-    | [ H : ?eq ?y ?x, H' : ?eq ?z ?y |- @equiv _ _ _ ?x ?z ] => trans y ; [ sym ; apply H | sym ; apply H' ]
-    | [ H : ?eq ?y ?x, H' : ?eq ?y ?z |- @equiv _ _ _ ?x ?z ] => trans y ; [ sym ; apply H | apply H' ]
-
-    | [ H : @equiv ?A ?R ?s ?x ?y |- @equiv _ _ _ ?y ?x ] => sym ; apply H
-    | [ |- @equiv _ _ _ ?x ?x ] => refl
-    | [ H : @equiv ?A ?R ?s ?x ?y, H' : @equiv ?A ?R ?s ?y ?z |- @equiv _ _ _ ?x ?z ] => trans y ; [ apply H | apply H' ]
-    | [ H : @equiv ?A ?R ?s ?x ?y, H' : @equiv ?A ?R ?s ?z ?y |- @equiv _ _ _ ?x ?z ] => trans y ; [ apply H | sym ; apply H' ]
-    | [ H : @equiv ?A ?R ?s ?y ?x, H' : @equiv ?A ?R ?s ?z ?y |- @equiv _ _ _ ?x ?z ] => trans y ; [ sym ; apply H | sym ; apply H' ]
-    | [ H : @equiv ?A ?R ?s ?y ?x, H' : @equiv ?A ?R ?s ?y ?z |- @equiv _ _ _ ?x ?z ] => trans y ; [ sym ; apply H | apply H' ]
-
-    | [ H : not (@equiv ?A ?R ?s ?X ?X) |- _ ] => elim H ; refl
-    | [ H : not (@equiv ?A ?R ?s ?X ?Y), H' : @equiv ?A ?R ?s ?Y ?X |- _ ] => elim H ; sym ; apply H
-    | [ H : not (@equiv ?A ?R ?s ?X ?Y), H' : ?R ?Y ?X |- _ ] => elim H ; sym ; apply H
-    | [ H : not (@equiv ?A ?R ?s ?X ?Y) |- False ] => elim H ; clear H ; setoid_tactic
-  end.
-(** Need to fix fresh to not fail if some arguments are not identifiers. *)
-(* Ltac setoid_sat ::= *)
-(*   match goal with *)
-(*     | [ H : ?x == ?y |- _ ] => let name:=fresh "Heq" y x in add_hypothesis name (equiv_sym H) *)
-(*     | [ H : ?x =/= ?y |- _ ] => let name:=fresh "Hneq" y x in add_hypothesis name (nequiv_sym H) *)
-(*     | [ H : ?x == ?y, H' : ?y == ?z |- _ ] => let name:=fresh "Heq" x z in add_hypothesis name (equiv_trans H H') *)
-(*     | [ H : ?x == ?y, H' : ?y =/= ?z |- _ ] => let name:=fresh "Hneq" x z in add_hypothesis name (equiv_nequiv H H') *)
-(*     | [ H : ?x =/= ?y, H' : ?y == ?z |- _ ] => let name:=fresh "Hneq" x z in add_hypothesis name (nequiv_equiv H H') *)
-(*   end. *)
-
-Ltac setoid_sat :=
-  match goal with
-    | [ H : ?x == ?y |- _ ] => let name:=fresh "Heq" in add_hypothesis name (equiv_sym H)
-    | [ H : ?x =/= ?y |- _ ] => let name:=fresh "Hneq" in add_hypothesis name (nequiv_sym H)
-    | [ H : ?x == ?y, H' : ?y == ?z |- _ ] => let name:=fresh "Heq" in add_hypothesis name (equiv_trans H H')
-    | [ H : ?x == ?y, H' : ?y =/= ?z |- _ ] => let name:=fresh "Hneq" in add_hypothesis name (equiv_nequiv H H')
-    | [ H : ?x =/= ?y, H' : ?y == ?z |- _ ] => let name:=fresh "Hneq" in add_hypothesis name (nequiv_equiv H H')
-  end.
-Ltac setoid_saturate := repeat setoid_sat.
-
diff --git a/theories/Program/Basics.v b/theories/Program/Basics.v
index e5bc98dee..014ff3a01 100644
--- a/theories/Program/Basics.v
+++ b/theories/Program/Basics.v
@@ -139,5 +139,3 @@ Tactic Notation "exist" constr(x) := exists x.
 Tactic Notation "exist" constr(x) constr(y) := exists x ; exists y.
 Tactic Notation "exist" constr(x) constr(y) constr(z) := exists x ; exists y ; exists z.
 Tactic Notation "exist" constr(x) constr(y) constr(z) constr(w) := exists x ; exists y ; exists z ; exists w.
-
-Notation " ! A " := (notT A) (at level 200, A at level 100) : type_scope.
diff --git a/toplevel/classes.ml b/toplevel/classes.ml
index d84fb3e56..92a5dfc8b 100644
--- a/toplevel/classes.ml
+++ b/toplevel/classes.ml
@@ -492,3 +492,60 @@ let _ =
     (fun env evd ev evi -> 
       Library.require_library [(dummy_loc, module_qualid)] None; (* may be inefficient *)
       solve_by_tac env evd ev evi (Lazy.force tactic))
+
+let prod = lazy (Coqlib.build_prod ())
+
+let build_conjunction evm =
+  List.fold_left
+    (fun (acc, evs) (ev, evi)  ->
+      if class_of_constr evi.evar_concl <> None then
+	mkApp ((Lazy.force prod).Coqlib.typ, [|evi.evar_concl; acc |]), evs
+      else acc, Evd.add evs ev evi)
+    (Coqlib.build_coq_True (), Evd.empty) evm
+
+let destruct_conjunction evm_list evm evm' term =
+  let _, evm =
+    List.fold_right
+      (fun (ev, evi) (term, evs) ->
+	if class_of_constr evi.evar_concl <> None then
+	  match kind_of_term term with
+	    | App (x, [| _ ; _ ; proof ; term |]) ->
+		let evs' = Evd.define evs ev proof in
+		  (term, evs')
+	    | _ -> assert(false)
+	else
+	  match (Evd.find evm' ev).evar_body with
+	      Evar_empty -> raise Not_found
+	    | Evar_defined c ->
+		let evs' = Evd.define evs ev c in
+		  (term, evs'))
+      evm_list (term, evm)
+  in evm
+ 
+(* let solve_by_tac env evd evar evi t = *)
+(*   let goal = {it = evi; sigma = (Evd.evars_of evd) } in *)
+(*   let (res, valid) = t goal in *)
+(*     if res.it = [] then *)
+(*       let prooftree = valid [] in *)
+(*       let proofterm, obls = Refiner.extract_open_proof res.sigma prooftree in *)
+(* 	if obls = [] then *)
+(* 	  let evd' = evars_reset_evd res.sigma evd in *)
+(* 	  let evd' = evar_define evar proofterm evd' in *)
+(* 	    evd', true *)
+(* 	else evd, false *)
+(*     else evd, false *)
+
+let resolve_all_typeclasses env evd =
+  let evm = Evd.evars_of evd in
+  let evm_list = Evd.to_list evm in
+  let goal, typesevm = build_conjunction evm_list in
+  let evars = ref (Evd.create_evar_defs typesevm) in
+  let term = resolve_one_typeclass_evd env evars goal in
+  let evm' = destruct_conjunction evm_list evm (Evd.evars_of !evars) term in
+    Evd.create_evar_defs evm'
+
+let _ =
+  Typeclasses.solve_instanciations_problem :=
+    (fun env evd -> 
+      Library.require_library [(dummy_loc, module_qualid)] None; (* may be inefficient *)
+      resolve_all_typeclasses env evd)
diff --git a/toplevel/classes.mli b/toplevel/classes.mli
index 93fc1b552..cfe881cb3 100644
--- a/toplevel/classes.mli
+++ b/toplevel/classes.mli
@@ -69,3 +69,5 @@ val push_named_context : named_context -> env -> env
 val name_typeclass_binders : Idset.t ->
     Topconstr.local_binder list ->
     Topconstr.local_binder list * Idset.t
+
+val resolve_all_typeclasses : env -> evar_defs -> evar_defs