- A little cleanup in Classes/*. Separate standard morphisms on

relf/sym/trans relations from morphisms on prop connectives and
relations.
- Add general order theory on predicates, instantiated for relations.
Derives equivalence, implication, conjunction and disjunction as
liftings from propositional connectives. Can be used for n-ary
homogeneous predicates thanks to a bit of metaprogramming with lists of
types. 
- Rebind Setoid_Theory to use the Equivalence record type instead of
declaring an isomorphic one. One needs to do "red" after constructor to
get the same statements when building objects of type Setoid_Theory, so
scripts break.


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

17 files changed, 648 insertions, 442 deletions

diff --git a/Makefile.common b/Makefile.common
index 11a7cbd0f..8421d397e 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -744,6 +744,7 @@ SETOIDSVO:= theories/Setoids/Setoid.vo # theories/Setoids/Setoid_tac.vo theories
 UNICODEVO:= theories/Unicode/Utf8.vo
 
 CLASSESVO:= theories/Classes/Init.vo theories/Classes/RelationClasses.vo theories/Classes/Morphisms.vo \
+	theories/Classes/Morphisms_Prop.vo theories/Classes/Morphisms_Relations.vo \
 	theories/Classes/Functions.vo theories/Classes/Equivalence.vo theories/Classes/SetoidTactics.vo \
 	theories/Classes/SetoidClass.vo theories/Classes/SetoidAxioms.vo theories/Classes/EquivDec.vo \
 	 theories/Classes/SetoidDec.vo
diff --git a/contrib/setoid_ring/Ring_theory.v b/contrib/setoid_ring/Ring_theory.v
index cefdcf52b..4c542ffdd 100644
--- a/contrib/setoid_ring/Ring_theory.v
+++ b/contrib/setoid_ring/Ring_theory.v
@@ -257,7 +257,7 @@ Section ALMOST_RING.
 
  (** Leibniz equality leads to a setoid theory and is extensional*)
  Lemma Eqsth : Setoid_Theory R (@eq R).
- Proof.  constructor;intros;subst;trivial. Qed.
+ Proof.  constructor;red;intros;subst;trivial. Qed.
 
  Lemma Eq_s_ext : sring_eq_ext radd rmul (@eq R).
  Proof. constructor;intros;subst;trivial. Qed.
diff --git a/contrib/setoid_ring/newring.ml4 b/contrib/setoid_ring/newring.ml4
index 7cf642ce7..c80b37d91 100644
--- a/contrib/setoid_ring/newring.ml4
+++ b/contrib/setoid_ring/newring.ml4
@@ -527,7 +527,7 @@ let ring_equality (r,add,mul,opp,req) =
 	  (setoid,op_morph)
     | _ ->
 	let setoid = setoid_of_relation (Global.env ()) r req in
-	let signature = [Some (r,req);Some (r,req)],Some(r,req) in
+	let signature = [Some (r,req);Some (r,req)],Some(Lazy.lazy_from_val (r,req)) in
 	let add_m, add_m_lem =
 	  try Class_tactics.default_morphism signature add
           with Not_found ->
@@ -540,7 +540,7 @@ let ring_equality (r,add,mul,opp,req) =
           match opp with
             | Some opp ->
 		(let opp_m,opp_m_lem =
-		  try Class_tactics.default_morphism ([Some(r,req)],Some(r,req)) opp
+		  try Class_tactics.default_morphism ([Some(r,req)],Some(Lazy.lazy_from_val (r,req))) opp
 		  with Not_found ->
                     error "ring opposite should be declared as a morphism" in
 		let op_morph =
@@ -830,7 +830,7 @@ let ring_lookup (f:glob_tactic_expr) lH rl t gl =
 TACTIC EXTEND ring_lookup
 | [ "ring_lookup" tactic(f) "[" constr_list(lH) "]" constr_list(lr)
       "[" constr(t) "]" ] ->
-          [ring_lookup (fst f) lH lr t]
+    [ring_lookup (fst f) lH lr t]
 END
 
 
@@ -1037,7 +1037,7 @@ let field_equality r inv req =
         mkApp((Coqlib.build_coq_eq_data()).congr,[|r;r;inv|])
     | _ ->
 	let _setoid = setoid_of_relation (Global.env ()) r req in
-	let signature = [Some (r,req)],Some(r,req) in
+	let signature = [Some (r,req)],Some(Lazy.lazy_from_val (r,req)) in
 	let inv_m, inv_m_lem =
 	  try Class_tactics.default_morphism signature inv
           with Not_found ->
diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4
index 075077048..bbd29e665 100644
--- a/tactics/class_tactics.ml4
+++ b/tactics/class_tactics.ml4
@@ -130,6 +130,7 @@ type search_state = {
   tacres : goal list sigma * validation;
   pri : int;
   last_tactic : std_ppcmds;
+(*   filter : constr -> constr -> bool; *)
   dblist : Auto.Hint_db.t list;
   localdb :  Auto.Hint_db.t list }
     
@@ -148,23 +149,23 @@ module SearchProblem = struct
       prlist (pr_ev evars) (sig_it gls)
 	
   let filter_tactics (glls,v) l =
-    if !debug then
-      (let _ = Proof_trees.db_pr_goal (List.hd (sig_it glls)) in
-      let evars = Evarutil.nf_evars (Refiner.project glls) in
-    	msg (str"Goal: " ++ pr_ev evars (List.hd (sig_it glls)) ++ str"\n"));
+(*     if !debug then *)
+(*       (let _ = Proof_trees.db_pr_goal (List.hd (sig_it glls)) in *)
+(*       let evars = Evarutil.nf_evars (Refiner.project glls) in *)
+(*     	msg (str"Goal: " ++ pr_ev evars (List.hd (sig_it glls)) ++ str"\n")); *)
     let rec aux = function
       | [] -> []
       | (tac,pri,pptac) :: tacl -> 
 	  try 
-	    if !debug then msg (str"\nTrying tactic: " ++ pptac ++ str"\n");
+(* 	    if !debug then msg (str"\nTrying tactic: " ++ pptac ++ str"\n"); *)
 	    let (lgls,ptl) = apply_tac_list tac glls in 
 	    let v' p = v (ptl p) in
-	      	      if !debug then
-	      		begin
-	      		  let evars = Evarutil.nf_evars (Refiner.project glls) in
-	      		    msg (str"\nOn goal: " ++ pr_ev evars (List.hd (sig_it glls)) ++ str"\n");
-	      		    msg (hov 1 (pptac ++ str" gives: \n" ++ pr_goals lgls ++ str"\n"))
-	      		end;
+(* 	      	      if !debug then *)
+(* 	      		begin *)
+(* 	      		  let evars = Evarutil.nf_evars (Refiner.project glls) in *)
+(* 	      		    msg (str"\nOn goal: " ++ pr_ev evars (List.hd (sig_it glls)) ++ str"\n"); *)
+(* 	      		    msg (hov 1 (pptac ++ str" gives: \n" ++ pr_goals lgls ++ str"\n")) *)
+(* 	      		end; *)
 	      ((lgls,v'),pri,pptac) :: aux tacl
 	  with e when Logic.catchable_exception e ->
 	    (* 	    if !debug then msg (str"failed\n"); *)
@@ -195,31 +196,33 @@ module SearchProblem = struct
       let nbgl = List.length (sig_it lg) in
       assert (nbgl > 0);
       let g = find_first_goal lg in
+(*       let filt = s.filter (pf_concl g) in *)
       let assumption_tacs = 
 	let l = 
 	  filter_tactics s.tacres
 	    (List.map 
 		(fun id -> (Eauto.e_give_exact_constr (mkVar id), 0,
 			   (str "exact" ++ spc () ++ pr_id id)))
-		(pf_ids_of_hyps g))
+(* 		(List.filter (fun id -> filt (pf_get_hyp_typ g id)) *)
+		    (pf_ids_of_hyps g))
 	in
 	  List.map (fun (res,pri,pp) -> { s with tacres = res; pri = 0;
 	    last_tactic = pp; localdb = List.tl s.localdb }) l
       in
-      let intro_tac = 
-	List.map 
-	  (fun ((lgls,_) as res,pri,pp) -> 
-	     let g' = first_goal lgls in 
-	     let hintl = 
-	       make_resolve_hyp (pf_env g') (project g') (pf_last_hyp g')
-	     in	       
-             let ldb = Hint_db.add_list hintl (match s.localdb with [] -> assert false | hd :: _ -> hd) in
-	       { s with tacres = res; 
-		 last_tactic = pp;
-		 pri = pri;
-		 localdb = ldb :: List.tl s.localdb })
-	  (filter_tactics s.tacres [Tactics.intro,1,(str "intro")])
-      in
+(*       let intro_tac =  *)
+(* 	List.map  *)
+(* 	  (fun ((lgls,_) as res,pri,pp) ->  *)
+(* 	     let g' = first_goal lgls in  *)
+(* 	     let hintl =  *)
+(* 	       make_resolve_hyp (pf_env g') (project g') (pf_last_hyp g') *)
+(* 	     in	        *)
+(*              let ldb = Hint_db.add_list hintl (match s.localdb with [] -> assert false | hd :: _ -> hd) in *)
+(* 	       { s with tacres = res;  *)
+(* 		 last_tactic = pp; *)
+(* 		 pri = pri; *)
+(* 		 localdb = ldb :: List.tl s.localdb }) *)
+(* 	  (filter_tactics s.tacres [Tactics.intro,1,(str "intro")]) *)
+(*       in *)
       let possible_resolve ((lgls,_) as res, pri, pp) =
 	let nbgl' = List.length (sig_it lgls) in
 	  if nbgl' < nbgl then
@@ -232,17 +235,13 @@ module SearchProblem = struct
 	      localdb = 
 		list_addn (nbgl'-nbgl) (List.hd s.localdb) s.localdb }
       in
-(*       let custom_tac =  *)
-(* 	List.map possible_resolve *)
-(* 	  (filter_tactics s.tacres [s.custom_tactic,(str "custom_tactic")]) *)
-(*       in *)
       let rec_tacs = 
 	let l = 
 	  filter_tactics s.tacres (e_possible_resolve s.dblist (List.hd s.localdb) (pf_concl g))
 	in
 	List.map possible_resolve l
       in
-      List.sort compare (assumption_tacs @ intro_tac (* @ custom_tac *) @ rec_tacs)
+      List.sort compare (assumption_tacs (* @intro_tac  @ custom_tac *) @ rec_tacs)
 
   let pp s = 
     msg (hov 0 (str " depth=" ++ int s.depth ++ spc () ++ 
@@ -252,10 +251,48 @@ end
 
 module Search = Explore.Make(SearchProblem)
 
+
+let filter_pat c =
+  try
+    let morg = Nametab.global (Qualid (dummy_loc, qualid_of_string "Coq.Classes.Morphisms.Morphism")) in
+    let morc = constr_of_global morg in
+	match kind_of_term c with
+	  | App(morph, [| t; r; m |]) when eq_constr morph morc ->
+	      (fun y ->
+		(match y.pat with
+		    Some (PApp (PRef mor, [| t'; r'; m' |])) when mor = morg ->
+		      (match m' with
+			| PRef c -> if isConst m then eq_constr (constr_of_global c) m else false
+			| _ -> true)
+		  | _ -> true))
+	  | _ -> fun _ -> true
+  with _ -> fun _ -> true
+
+let morphism_class = 
+  lazy (class_info (Nametab.global (Qualid (dummy_loc, qualid_of_string "Coq.Classes.Morphisms.Morphism"))))
+    
+let filter c =
+  try let morc = constr_of_global (Nametab.global (Qualid (dummy_loc, qualid_of_string "Coq.Classes.Morphisms.Morphism"))) in
+	match kind_of_term c with
+	  | App(morph, [| t; r; m |]) when eq_constr morph morc ->
+	      (fun y ->
+		let (_, r) = decompose_prod y in
+		  (match kind_of_term r with
+		      App (morph', [| t'; r'; m' |]) when eq_constr morph' morc ->
+			(match kind_of_term m' with
+			  | Rel n -> true
+			  | Const c -> eq_constr m m'
+			  | App _ -> true
+			  | _ -> false)
+		    | _ -> false))
+	  | _ -> fun _ -> true
+  with _ -> fun _ -> true
+
 let make_initial_state n gls dblist localdbs =
   { depth = n;
     tacres = gls;
     pri = 0;
+(*     filter = filter; *)
     last_tactic = (mt ());
     dblist = dblist;
     localdb = localdbs }
@@ -422,9 +459,6 @@ END
 
 (** Typeclass-based rewriting. *)
 
-let morphism_class = 
-  lazy (class_info (Nametab.global (Qualid (dummy_loc, qualid_of_string "Coq.Classes.Morphisms.Morphism"))))
-
 let respect_proj = lazy (mkConst (List.hd (Lazy.force morphism_class).cl_projs))
 
 let make_dir l = make_dirpath (List.map id_of_string (List.rev l))
@@ -499,7 +533,7 @@ let split_head = function
     hd :: tl -> hd, tl
   | [] -> assert(false)
 
-let build_signature isevars env m (cstrs : 'a option list) (finalcstr : 'a option) (f : 'a -> constr) =
+let build_signature isevars env m (cstrs : 'a option list) (finalcstr : 'a Lazy.t option) (f : 'a -> constr) =
   let new_evar isevars env t =
     Evarutil.e_new_evar isevars env
       (* ~src:(dummy_loc, ImplicitArg (ConstRef (Lazy.force respectful), (n, Some na))) *) t
@@ -527,7 +561,8 @@ let build_signature isevars env m (cstrs : 'a option list) (finalcstr : 'a optio
 		let t = Reductionops.nf_betaiota t in
 		let rel = mk_relty t None in 
 		  t, rel, [t, rel]
-	    | Some (t, rel) -> t, rel, [t, rel])
+	    | Some codom -> let (t, rel) = Lazy.force codom in
+			      t, rel, [t, rel])
   in aux m cstrs
 
 let reflexivity_proof_evar env evars carrier relation x =
@@ -554,26 +589,17 @@ let reflexive_proof env = find_class_proof reflexive_type reflexive_proof env
 let symmetric_proof env = find_class_proof symmetric_type symmetric_proof env
 let transitive_proof env = find_class_proof transitive_type transitive_proof env
 
+exception FoundInt of int
+
+let array_find (arr: 'a array) (pred: int -> 'a -> bool): int = 
+  try
+    for i=0 to Array.length arr - 1 do if pred i (arr.(i)) then raise (FoundInt i) done;
+    raise Not_found
+  with FoundInt i -> i
+
 let resolve_morphism env sigma oldt m ?(fnewt=fun x -> x) args args' cstr evars =
   let morph_instance, proj, sigargs, m', args, args' = 
-(*     if is_equiv env sigma m then  *)
-(*       let params, rest = array_chop 3 args in *)
-(*       let a, r, s = params.(0), params.(1), params.(2) in *)
-(*       let params', rest' = array_chop 3 args' in *)
-(*       let inst = mkApp (Lazy.force setoid_morphism, params) in *)
-(* 	(* Equiv gives a binary morphism *) *)
-(*       let (cl, proj) = Lazy.force class_two in *)
-(*       let ctxargs = [ a; r; s; a; r; s; mkProp; Lazy.force iff; Lazy.force iff_setoid; ] in *)
-(*       let m' = mkApp (m, [| a; r; s |]) in *)
-(* 	inst, proj, ctxargs, m', rest, rest' *)
-(*     else *)
-    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
+    let first = try (array_find args' (fun i b -> b <> None)) with Not_found -> raise (Invalid_argument "resolve_morphism") in
     let morphargs, morphobjs = array_chop first args in
     let morphargs', morphobjs' = array_chop first args' in
     let appm = mkApp(m, morphargs) in
@@ -736,9 +762,47 @@ let unfold_all t =
 	  | _ -> assert false)
     | _ -> assert false
 
-type rewrite_flags = { under_lambdas : bool }
+(* let lift_cstr env sigma evars args cstr = *)
+(*   let codom =  *)
+(*     match cstr with *)
+(*       | Some c -> c *)
+(*       | None -> *)
+(* 	  let ty = Evarutil.e_new_evar evars env (new_Type ()) in *)
+(* 	  let rel = Evarutil.e_new_evar evars env (mk_relation ty) in *)
+(* 	    (ty, rel) *)
+(*   in *)
+(*     Array.fold_right *)
+(*       (fun arg (car, rel) ->  *)
+(* 	let ty = Typing.type_of env sigma arg in *)
+(* 	let car' = mkProd (Anonymous, ty, car) in *)
+(* 	let rel' = mkApp (Lazy.force pointwise_relation, [| ty; car; rel |]) in *)
+(* 	  (car', rel')) *)
+(*       args codom *)
+
+let rec decomp_pointwise n c =
+  if n = 0 then c
+  else
+    match kind_of_term c with
+      | App (pointwise, [| a; b; relb |]) -> decomp_pointwise (pred n) relb
+      | _ -> raise Not_found
+	  
+let lift_cstr env sigma evars args cstr =
+  match cstr with
+    | Some codom -> 
+	let cstr () =
+	  Array.fold_right
+	    (fun arg (car, rel) -> 
+	      let ty = Typing.type_of env sigma arg in
+	      let car' = mkProd (Anonymous, ty, car) in
+	      let rel' = mkApp (Lazy.force pointwise_relation, [| ty; car; rel |]) in
+		(car', rel'))
+	    args (Lazy.force codom)
+	in Some (Lazy.lazy_from_fun cstr)
+    | None -> None
+	  
+type rewrite_flags = { under_lambdas : bool; on_morphisms : bool }
 
-let default_flags = { under_lambdas = true }
+let default_flags = { under_lambdas = true; on_morphisms = true; }
 
 let build_new gl env sigma flags occs hypinfo concl cstr evars =
   let is_occ occ = occs = [] || List.mem occ occs in
@@ -763,19 +827,36 @@ let build_new gl env sigma flags occs hypinfo concl cstr evars =
       | None -> 
 	  match kind_of_term t with
 	    | App (m, args) ->
-		let args', occ = 
-		  Array.fold_left 
-		    (fun (acc, occ) arg -> let res, occ = aux env arg occ None in (res :: acc, occ))
-		    ([], occ) args
+		let rewrite_args () = 
+		  let args', occ = 
+		    Array.fold_left 
+		      (fun (acc, occ) arg -> let res, occ = aux env arg occ None in (res :: acc, occ))
+		      ([], occ) args
+		  in
+		  let res =
+		    if List.for_all (fun x -> x = None) args' then None
+		    else 
+		      let args' = Array.of_list (List.rev args') in
+			(try Some (resolve_morphism env sigma t m args args' cstr evars)
+			  with Not_found -> None)
+		  in res, occ
 		in
-		let res =
-		  if List.for_all (fun x -> x = None) args' then None
-		  else 
-		    let args' = Array.of_list (List.rev args') in
-		      (try Some (resolve_morphism env sigma t m args args' cstr evars)
-			with Not_found -> None)
-		in res, occ
-		  
+		  if flags.on_morphisms then
+		    let m', occ = aux env m occ (lift_cstr env sigma evars args cstr) in
+		      match m' with
+			  None -> rewrite_args () (* Standard path, try rewrite on arguments *)
+			| Some (prf, (car, rel, c1, c2)) -> 
+			    (* We rewrote the function and get a proof of pointwise rel for the arguments.
+			       We just apply it. *)
+			    let nargs = Array.length args in
+			    let decompprod c = snd (Reductionops.decomp_n_prod env (Evd.evars_of !evars) nargs c) in
+			    let res = 
+			      try Some (mkApp (prf, args),
+				       (decompprod car, decomp_pointwise nargs rel, mkApp(c1, args), mkApp(c2, args)))
+			      with Not_found -> None
+			    in res, occ
+		  else rewrite_args ()
+		    
 	    | Prod (_, x, b) when not (dependent (mkRel 1) b) -> 
 		let x', occ = aux env x occ None in
 		let b', occ = aux env b occ None in
@@ -832,8 +913,6 @@ let resolve_typeclass_evars d p env evd onlyargs =
       (fun ev evi -> class_of_constr evi.Evd.evar_concl <> None)
   in resolve_all_evars d p env pred evd
       
-let cl_rewrite_tactic = lazy (Tacinterp.interp <:tactic<setoid_rewrite_tac>>)
-
 let cl_rewrite_clause_aux ?(flags=default_flags) hypinfo goal_meta occs clause gl =
   let concl, is_hyp = 
     match clause with
@@ -848,7 +927,7 @@ let cl_rewrite_clause_aux ?(flags=default_flags) hypinfo goal_meta occs clause g
   let evars = ref (Evd.create_evar_defs Evd.empty) in
   let env = pf_env gl in
   let sigma = project gl in
-  let eq, _ = build_new gl env sigma flags occs hypinfo concl (Some cstr) evars in
+  let eq, _ = build_new gl env sigma flags occs hypinfo concl (Some (Lazy.lazy_from_val cstr)) evars in
     match eq with  
 	Some (p, (_, _, oldt, newt)) -> 
 	  (try 
@@ -1322,7 +1401,7 @@ let get_hyp gl c clause l2r =
 	  unification_rewrite hi.l2r hi.c1 hi.c2 hi.cl hi.rel but gl
     | _ -> decompose_setoid_eqhyp (pf_env gl) (project gl) c l2r
 	
-let general_rewrite_flags = { under_lambdas = false }
+let general_rewrite_flags = { under_lambdas = false; on_morphisms = false }
 
 let general_s_rewrite l2r c ~new_goals gl =
   let meta = Evarutil.new_meta() in
diff --git a/theories/Classes/Equivalence.v b/theories/Classes/Equivalence.v
index 0ec6c11f9..d7774a2d7 100644
--- a/theories/Classes/Equivalence.v
+++ b/theories/Classes/Equivalence.v
@@ -35,23 +35,25 @@ Instance [ Equivalence A R ] =>
 
 Definition equiv [ Equivalence A R ] : relation A := R.
 
-(** Shortcuts to make proof search possible (unification won't unfold equiv). *)
+Typeclasses unfold @equiv.
 
-Program Instance [ sa : Equivalence A ] => equiv_refl : Reflexive equiv.
+(* (** Shortcuts to make proof search possible (unification won't unfold equiv). *) *)
 
-Program Instance [ sa : Equivalence A ] => equiv_sym : Symmetric equiv.
+(* Program Instance [ sa : Equivalence A ] => equiv_refl : Reflexive equiv. *)
 
-  Next Obligation.
-  Proof.
-    symmetry ; auto.
-  Qed.
+(* Program Instance [ sa : Equivalence A ] => equiv_sym : Symmetric equiv. *)
 
-Program Instance [ sa : Equivalence A ] => equiv_trans : Transitive equiv.
+(*   Next Obligation. *)
+(*   Proof. *)
+(*     symmetry ; auto. *)
+(*   Qed. *)
 
-  Next Obligation.
-  Proof.
-    transitivity y ; auto.
-  Qed.
+(* Program Instance [ sa : Equivalence A ] => equiv_trans : Transitive equiv. *)
+
+(*   Next Obligation. *)
+(*   Proof. *)
+(*     transitivity y ; auto. *)
+(*   Qed. *)
 
 (** Overloaded notations for setoid equivalence and inequivalence. Not to be confused with [eq] and [=]. *)
 
@@ -64,23 +66,6 @@ Notation " x =/= y " := (complement equiv x y) (at level 70, no associativity) :
   
 Open Local Scope equiv_scope.
 
-(** Use the [clsubstitute] command which substitutes an equality in every hypothesis. *)
-
-Ltac setoid_subst H := 
-  match type of H with
-    ?x === ?y => substitute H ; clear H x
-  end.
-
-Ltac setoid_subst_nofail :=
-  match goal with
-    | [ H : ?x === ?y |- _ ] => setoid_subst H ; setoid_subst_nofail
-    | _ => idtac
-  end.
-  
-(** [subst*] will try its best at substituting every equality in the goal. *)
-
-Tactic Notation "subst" "*" := subst_no_fail ; setoid_subst_nofail.
-
 Lemma nequiv_equiv_trans : forall [ Equivalence A ] (x y z : A), x =/= y -> y === z -> x =/= z.
 Proof with auto.
   intros; intro.
@@ -97,6 +82,23 @@ Proof.
   contradiction.
 Qed.
 
+(** Use the [substitute] command which substitutes an applied relation in every hypothesis. *)
+
+Ltac setoid_subst H := 
+  match type of H with
+    ?x === ?y => substitute H ; clear H x
+  end.
+
+Ltac setoid_subst_nofail :=
+  match goal with
+    | [ H : ?x === ?y |- _ ] => setoid_subst H ; setoid_subst_nofail
+    | _ => idtac
+  end.
+  
+(** [subst*] will try its best at substituting every equality in the goal. *)
+
+Tactic Notation "subst" "*" := subst_no_fail ; setoid_subst_nofail.
+
 Ltac equiv_simplify_one :=
   match goal with
     | [ H : ?x === ?x |- _ ] => clear H
@@ -117,34 +119,28 @@ Ltac equivify := repeat equivify_tac.
 
 (** Every equivalence relation gives rise to a morphism, as it is Transitive and Symmetric. *)
 
-Instance [ sa : Equivalence ] => equiv_morphism : Morphism (equiv ++> equiv ++> iff) equiv :=
-  respect := respect.
-
-(** The partial application too as it is Reflexive. *)
+(* Instance [ sa : Equivalence ] => equiv_morphism : Morphism (equiv ++> equiv ++> iff) equiv := *)
+(*   respect := respect. *)
 
-Instance [ sa : Equivalence A ] (x : A) => 
-  equiv_partial_app_morphism : Morphism (equiv ++> iff) (equiv x) :=
-  respect := respect. 
+(* (** The partial application too as it is Reflexive. *) *)
 
-Definition type_eq : relation Type :=
-  fun x y => x = y.
+(* Instance [ sa : Equivalence A ] (x : A) =>  *)
+(*   equiv_partial_app_morphism : Morphism (equiv ++> iff) (equiv x) := *)
+(*   respect := respect.  *)
 
-Program Instance type_equivalence : Equivalence Type type_eq.
+(** Instance not exported by default, as comparing types for equivalence may be unintentional. *)
 
-  Solve Obligations using constructor ; unfold type_eq ; program_simpl.
+Section Type_Equivalence.
 
-Ltac morphism_tac := try red ; unfold arrow ; intros ; program_simpl ; try tauto.
-
-Ltac obligations_tactic ::= morphism_tac.
-
-(** These are morphisms used to rewrite at the top level of a proof, 
-   using [iff_impl_id_morphism] if the proof is in [Prop] and
-   [eq_arrow_id_morphism] if it is in Type. *)
-
-Program Instance iff_impl_id_morphism : 
-  Morphism (iff ++> impl) id.
+  Definition type_eq : relation Type :=
+    fun x y => x = y.
+  
+  Program Instance type_equivalence : Equivalence Type type_eq.
+  
+  Next Obligation. 
+  Proof. unfold type_eq in *. subst. reflexivity. Qed.
 
-(* Program Instance eq_arrow_id_morphism : ? Morphism (eq +++> arrow) id. *)
+End Type_Equivalence.
 
 (** Partial equivs don't require reflexivity so we can build a partial equiv on the function space. *)
 
@@ -152,11 +148,32 @@ Class PartialEquivalence (carrier : Type) (pequiv : relation carrier) :=
   pequiv_prf :> PER carrier pequiv.
 
 Definition pequiv [ PartialEquivalence A R ] : relation A := R.
+Typeclasses unfold @pequiv.
 
 (** Overloaded notation for partial equiv equivalence. *)
 
 Notation " x =~= y " := (pequiv x y) (at level 70, no associativity) : type_scope.
 
-(** Reset the default Program tactic. *)
+Section Respecting.
+
+  (** Here we build an equivalence instance for functions which relates respectful ones only, 
+     we do not export it. *)
+
+  Definition respecting [ Equivalence A (R : relation A), Equivalence B (R' : relation B) ] : Type := 
+    { morph : A -> B | respectful R R' morph morph }.
+  
+  Program Instance [ Equivalence A R, Equivalence B R' ] => 
+    respecting_equiv : Equivalence respecting
+    (fun (f g : respecting) => forall (x y : A), R x y -> R' (proj1_sig f x) (proj1_sig g y)).
+
+  Solve Obligations using unfold respecting in * ; simpl_relation ; program_simpl.
+
+  Next Obligation.
+  Proof. 
+    unfold respecting in *. program_simpl. red in H2,H3,H4. 
+    transitivity (y x0) ; auto.
+    transitivity (y y0) ; auto.
+    symmetry. auto.
+  Qed.
 
-Ltac obligations_tactic ::= program_simpl.
+End Respecting.
\ No newline at end of file
diff --git a/theories/Classes/Morphisms.v b/theories/Classes/Morphisms.v
index d10cb9724..7cabc836d 100644
--- a/theories/Classes/Morphisms.v
+++ b/theories/Classes/Morphisms.v
@@ -1,4 +1,4 @@
-(* -*- coq-prog-args: ("-emacs-U" "-top" "Coq.Classes.Morphisms") -*- *)
+(* -*- coq-prog-args: ("-emacs-U" "-top" "Coq.Classes.Morphisms"); compile-command: "make -C ../.. TIME='time'" -*- *)
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
 (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
@@ -7,7 +7,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* Typeclass-based morphisms with standard instances for equivalence relations.
+(* Typeclass-based morphism definition and standard, minimal instances.
  
    Author: Matthieu Sozeau
    Institution: LRI, CNRS UMR 8623 - UniversitÃcopyright Paris Sud
@@ -26,7 +26,7 @@ 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. *)
+   These will be used by the [setoid_rewrite] tactic later. *)
 
 (** Respectful morphisms. *)
 
@@ -71,49 +71,6 @@ Class Morphism A (R : relation A) (m : A) : Prop :=
 
 Arguments Scope Morphism [type_scope signature_scope].
 
-(** 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, Equivalence B R' ] => 
-  respecting_equiv : Equivalence respecting
-  (fun (f g : respecting) => forall (x y : A), R x y -> R' (proj1_sig f x) (proj1_sig g y)).
-
-  Next Obligation.
-  Proof.
-    red ; intros.
-    destruct x ; simpl.
-    apply r ; auto.
-  Qed.
-
-  Next Obligation.
-  Proof.
-    red ; intros.
-    symmetry ; apply H.
-    symmetry ; auto.
-  Qed.
-
-  Next Obligation.
-  Proof.
-    red ; intros.
-    transitivity (proj1_sig y y0).
-    apply H ; auto.
-    apply H0. reflexivity.
-  Qed.
-
-(** Can't use the definition [notT] as it gives a universe inconsistency. *)
-
-Ltac obligations_tactic ::= program_simpl ; simpl_relation.
-
-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].
@@ -139,41 +96,41 @@ Proof. firstorder. Qed.
 
 (** [Morphism] is itself a covariant morphism for [subrelation]. *)
 
-Lemma subrelation_morphism [ subrelation A R₁ R₂, ! Morphism R₁ m ] : Morphism R₂ m.
+Lemma subrelation_morphism [ sub : subrelation A R₁ R₂, mor : Morphism A R₁ m ] : Morphism R₂ m.
 Proof.
-  intros. apply* H. apply H0.
+  intros. apply sub. apply mor.
 Qed.
 
 Instance morphism_subrelation_morphism : 
   Morphism (subrelation ++> @eq _ ==> impl) (@Morphism A).
 Proof. reduce. subst. firstorder. Qed.
 
-Inductive done : nat -> Type :=
-  did : forall n : nat, done n.
+(** We use an external tactic to manage the application of subrelation, which is otherwise
+   always applicable. We allow its use only once per branch. *)
+
+Inductive subrelation_done : Prop :=
+  did_subrelation : subrelation_done.
 
 Ltac subrelation_tac := 
   match goal with
-    | [ H : done 1 |- @Morphism _ _ _ ] => fail
+    | [ H : subrelation_done |- _ ] => fail
     | [ |- @Morphism _ _ _ ] => let H := fresh "H" in
-      set(H:=did 1) ; eapply @subrelation_morphism
+      set(H:=did_subrelation) ; eapply @subrelation_morphism
   end.
 
-(* Hint Resolve @subrelation_morphism 4 : typeclass_instances. *)
-
 Hint Extern 4 (@Morphism _ _ _) => subrelation_tac : typeclass_instances.
 
-(** Logical implication [impl] is a morphism for logical equivalence. *)
+(** Essential subrelation instances for [iff], [impl] and [pointwise_relation]. *)
 
-Program Instance iff_iff_iff_impl_morphism : Morphism (iff ==> iff ==> iff) impl.
+Instance iff_impl_subrelation : subrelation iff impl.
+Proof. firstorder. Qed.
 
-(* Typeclasses eauto := debug. *)
+Instance iff_inverse_impl_subrelation : subrelation iff (inverse impl).
+Proof. firstorder. Qed.
 
-Program Instance [ Symmetric A R, Morphism _ (R ==> impl) m ] => Reflexive_impl_iff : Morphism (R ==> iff) m.
-
-  Next Obligation.
-  Proof.
-    split ; apply respect ; [ auto | symmetry ] ; auto.
-  Qed.
+Instance [ subrelation A R R' ] => pointwise_subrelation :
+  subrelation (pointwise_relation (A:=B) R) (pointwise_relation R') | 4.
+Proof. reduce. unfold pointwise_relation in *. apply subrelation0. apply H. Qed.
 
 (** The complement of a relation conserves its morphisms. *)
 
@@ -183,28 +140,26 @@ Program Instance [ mR : Morphism (A -> A -> Prop) (RA ==> RA ==> iff) R ] =>
   Next Obligation.
   Proof.
     unfold complement.
-    pose (respect).
-    pose (r x y H).
-    pose (r0 x0 y0 H0).
+    pose (mR x y H x0 y0 H0).
     intuition.
   Qed.
 
 (** The inverse too. *)
 
-Program Instance [ Morphism (A -> _) (RA ==> RA ==> iff) R ] => 
+Program Instance [ mor : Morphism (A -> _) (RA ==> RA ==> iff) R ] => 
   inverse_morphism : Morphism (RA ==> RA ==> iff) (inverse R).
 
   Next Obligation.
   Proof.
-    apply respect ; auto.
+    apply mor ; auto.
   Qed.
 
-Program Instance [ Morphism (A -> B -> C) (RA ==> RB ==> RC) f ] => 
+Program Instance [ mor : Morphism (A -> B -> C) (RA ==> RB ==> RC) f ] => 
   flip_morphism : Morphism (RB ==> RA ==> RC) (flip f).
 
   Next Obligation.
   Proof.
-    apply respect ; auto.
+    apply mor ; auto.
   Qed.
 
 (** Every Transitive relation gives rise to a binary morphism on [impl], 
@@ -229,18 +184,6 @@ Program Instance [ Transitive A R ] =>
     apply* trans_contra_co_morphism ; eauto. eauto.
   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. *)
-
-
 (** Morphism declarations for partial applications. *)
 
 Program Instance [ Transitive A R ] (x : A) =>
@@ -286,18 +229,6 @@ Program Instance [ Equivalence A R ] (x : A) =>
     symmetry...
   Qed.
 
-(** With Symmetric relations, variance is no issue ! *)
-
-(* Program Instance (A B : Type) (R : relation A) (R' : relation B) *)
-(*   [ Morphism _ (R ==> R') m ] [ Symmetric A R ] =>  *)
-(*   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 [ Morphism (A -> B) (R ==> R') m, Reflexive _ R ] (x : A) =>
@@ -360,57 +291,9 @@ Program Instance 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_inverse_impl_iff_morphism : 
-  Morphism (inverse impl ==> iff ==> inverse impl) and.
-
-Program Instance and_iff_inverse_impl_morphism : 
-  Morphism (iff ==> inverse impl ==> inverse 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_inverse_impl_iff_morphism :
-  Morphism (inverse impl ==> iff ==> inverse impl) or.
-
-Program Instance or_iff_inverse_impl_morphism : 
-  Morphism (iff ==> inverse impl ==> inverse impl) or.
-
-Program Instance or_iff_morphism : 
-  Morphism (iff ==> iff ==> iff) or.
-
 (** Coq functions are morphisms for leibniz equality, 
    applied only if really needed. *)
 
-(* Instance {A B : Type} (m : A -> B) => *)
-(*   any_eq_eq_morphism : Morphism (@Logic.eq A ==> @Logic.eq B) m | 4. *)
-(* Proof. *)
-(*   red ; intros. subst ; reflexivity. *)
-(* Qed. *)
-
-(* Instance {A : Type} (m : A -> Prop) => *)
-(*   any_eq_iff_morphism : Morphism (@Logic.eq A ==> iff) m | 4. *)
-(* Proof. *)
-(*   red ; intros. subst ; split; trivial. *)
-(* Qed. *)
-
 Instance (A : Type) [ Reflexive B R ] (m : A -> B) =>
   eq_reflexive_morphism : Morphism (@Logic.eq A ==> R) m | 3.
 Proof. simpl_relation. Qed.
@@ -419,18 +302,13 @@ Instance (A : Type) [ Reflexive B R' ] =>
   Reflexive (@Logic.eq A ==> R').
 Proof. simpl_relation. Qed.
 
-Instance [ Morphism (A -> B) (inverse R ==> R') m ] =>
-  Morphism (R ==> inverse R') m | 10.
-Proof. firstorder. Qed.
-
 (** [respectful] is a morphism for relation equivalence. *)
 
 Instance respectful_morphism : 
   Morphism (relation_equivalence ++> relation_equivalence ++> relation_equivalence) (@respectful A B). 
 Proof.
-  do 2 red ; intros.
-  unfold respectful, relation_equivalence in *.
-  red ; intros.
+  reduce.
+  unfold respectful, relation_equivalence, predicate_equivalence in * ; simpl in *.
   split ; intros.
   
     rewrite <- H0.
@@ -452,21 +330,18 @@ Proof.
   split ; intros ; intuition.
 Qed.
 
+
 Class (A : Type) (R : relation A) => Normalizes (m : A) (m' : A) : Prop :=
   normalizes : R m m'.
 
 Instance (A : Type) (R : relation A) (B : Type) (R' : relation B) =>
-  Normalizes relation_equivalence (inverse R ==> inverse R') (inverse (R ==> R')) .
-Proof.
-  reduce.
-  symmetry ; apply inverse_respectful.
-Qed.
+  Normalizes subrelation (inverse R ==> inverse R') (inverse (R ==> R')) .
+Proof. simpl_relation. Qed.
 
 Instance [ Normalizes (relation B) relation_equivalence R' (inverse R'') ] =>
   ! Normalizes (relation (A -> B)) relation_equivalence (inverse R ==> R') (inverse (R ==> R'')) .
-Proof.
-  red.
-  pose normalizes.
+Proof. red ; intros. 
+  pose normalizes as r.
   setoid_rewrite r.
   setoid_rewrite inverse_respectful.
   reflexivity.
@@ -479,23 +354,23 @@ Program Instance [ Morphism A R m ] =>
 
 Instance morphism_morphism : Morphism (relation_equivalence ==> @eq _ ==> iff) (@Morphism A).
 Proof.
-  simpl_relation. 
-  unfold relation_equivalence in H.
+  simpl_relation.
+  reduce in H.
   split ; red ; intros.
   setoid_rewrite <- H.
-  apply respect.
+  apply H0.
   setoid_rewrite H.
-  apply respect.
+  apply H0.
 Qed.
-  
+
 Lemma morphism_releq_morphism 
   [ Normalizes (relation A) relation_equivalence R R',
     Morphism _ R' m ] : Morphism R m.
 Proof.
   intros.
-  pose respect.
-  assert(n:=normalizes).
-  setoid_rewrite n.
+  pose respect as r.
+  pose normalizes as norm.
+  setoid_rewrite norm.
   assumption.
 Qed.
 
@@ -510,86 +385,3 @@ Ltac morphism_normalization :=
 
 Hint Extern 5 (@Morphism _ _ _) => morphism_normalization : typeclass_instances.
 
-(** Morphisms for relations *)
-
-Instance [ PartialOrder A eqA R ] => 
-   partial_order_morphism : Morphism (eqA ==> eqA ==> iff) R.
-Proof with auto.
-  intros. rewrite partial_order_equivalence.
-  simpl_relation. firstorder.
-    transitivity x... transitivity x0... 
-    transitivity y... transitivity y0...
-Qed.
-
-Instance Morphism (relation_equivalence (A:=A) ==> 
-  relation_equivalence ==> relation_equivalence) relation_conjunction.
-  Proof. firstorder. Qed.
-
-Instance Morphism (relation_equivalence (A:=A) ==> 
-  relation_equivalence ==> relation_equivalence) relation_disjunction.
-  Proof. firstorder. Qed.
-
-
-(** Morphisms for quantifiers *)
-
-Program Instance {A : Type} => ex_iff_morphism : Morphism (pointwise_relation iff ==> iff) (@ex A).
-
-  Next Obligation.
-  Proof.
-    unfold pointwise_relation in H.     
-    split ; intros.
-    destruct H0 as [x₁ H₁].
-    exists x₁. rewrite H in H₁. assumption.
-    
-    destruct H0 as [x₁ H₁].
-    exists x₁. rewrite H. assumption.
-  Qed.
-
-Program Instance {A : Type} => ex_impl_morphism :
-  Morphism (pointwise_relation impl ==> impl) (@ex A).
-
-  Next Obligation.
-  Proof.
-    unfold pointwise_relation in H.  
-    exists H0. apply H. assumption.
-  Qed.
-
-Program Instance {A : Type} => ex_inverse_impl_morphism : 
-  Morphism (pointwise_relation (inverse impl) ==> inverse impl) (@ex A).
-
-  Next Obligation.
-  Proof.
-    unfold pointwise_relation in H.  
-    exists H0. apply H. assumption.
-  Qed.
-
-Program Instance {A : Type} => all_iff_morphism : 
-  Morphism (pointwise_relation iff ==> iff) (@all A).
-
-  Next Obligation.
-  Proof.
-    unfold pointwise_relation, all in *.
-    intuition ; specialize (H x0) ; intuition.
-  Qed.
-
-Program Instance {A : Type} => all_impl_morphism : 
-  Morphism (pointwise_relation impl ==> impl) (@all A).
-  
-  Next Obligation.
-  Proof.
-    unfold pointwise_relation, all in *.
-    intuition ; specialize (H x0) ; intuition.
-  Qed.
-
-Program Instance {A : Type} => all_inverse_impl_morphism : 
-  Morphism (pointwise_relation (inverse impl) ==> inverse impl) (@all A).
-  
-  Next Obligation.
-  Proof.
-    unfold pointwise_relation, all in *.
-    intuition ; specialize (H x0) ; intuition.
-  Qed.
-
-Lemma inverse_pointwise_relation A (R : relation A) : 
-  relation_equivalence (pointwise_relation (inverse R)) (inverse (pointwise_relation (A:=A) R)).
-Proof. reflexivity. Qed.
diff --git a/theories/Classes/Morphisms_Prop.v b/theories/Classes/Morphisms_Prop.v
new file mode 100644
index 000000000..d22ab06cb
--- /dev/null
+++ b/theories/Classes/Morphisms_Prop.v
@@ -0,0 +1,131 @@
+(* -*- coq-prog-args: ("-emacs-U" "-top" "Coq.Classes.Morphisms") -*- *)
+(************************************************************************)
+(*  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        *)
+(************************************************************************)
+
+(* Morphism instances for propositional connectives.
+ 
+   Author: Matthieu Sozeau
+   Institution: LRI, CNRS UMR 8623 - UniversitÃcopyright Paris Sud
+   91405 Orsay, France *)
+
+Require Import Coq.Classes.Morphisms.
+Require Import Coq.Program.Program.
+
+(** Standard instances for [not], [iff] and [impl]. *)
+
+(** Logical negation. *)
+
+Program Instance not_impl_morphism :
+  Morphism (impl --> impl) not.
+
+Program Instance not_iff_morphism : 
+  Morphism (iff ++> iff) not.
+
+(** Logical conjunction. *)
+
+Program Instance and_impl_iff_morphism :
+  Morphism (impl ==> impl ==> impl) and.
+
+(* 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_inverse_impl_iff_morphism :  *)
+(*   Morphism (inverse impl ==> iff ==> inverse impl) and. *)
+
+(* Program Instance and_iff_inverse_impl_morphism :  *)
+(*   Morphism (iff ==> inverse impl ==> inverse impl) and. *)
+
+Program Instance and_iff_morphism : 
+  Morphism (iff ==> iff ==> iff) and.
+
+(** Logical disjunction. *)
+
+Program Instance or_impl_iff_morphism : 
+  Morphism (impl ==> impl ==> impl) or.
+
+(* 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_inverse_impl_iff_morphism : *)
+(*   Morphism (inverse impl ==> iff ==> inverse impl) or. *)
+
+(* Program Instance or_iff_inverse_impl_morphism :  *)
+(*   Morphism (iff ==> inverse impl ==> inverse impl) or. *)
+
+Program Instance or_iff_morphism : 
+  Morphism (iff ==> iff ==> iff) or.
+
+(** Logical implication [impl] is a morphism for logical equivalence. *)
+
+Program Instance iff_iff_iff_impl_morphism : Morphism (iff ==> iff ==> iff) impl.
+
+(** Morphisms for quantifiers *)
+
+Program Instance {A : Type} => ex_iff_morphism : Morphism (pointwise_relation iff ==> iff) (@ex A).
+
+  Next Obligation.
+  Proof.
+    unfold pointwise_relation in H.     
+    split ; intros.
+    destruct H0 as [x₁ H₁].
+    exists x₁. rewrite H in H₁. assumption.
+    
+    destruct H0 as [x₁ H₁].
+    exists x₁. rewrite H. assumption.
+  Qed.
+
+Program Instance {A : Type} => ex_impl_morphism :
+  Morphism (pointwise_relation impl ==> impl) (@ex A).
+
+  Next Obligation.
+  Proof.
+    unfold pointwise_relation in H.  
+    exists H0. apply H. assumption.
+  Qed.
+
+Program Instance {A : Type} => ex_inverse_impl_morphism : 
+  Morphism (pointwise_relation (inverse impl) ==> inverse impl) (@ex A).
+
+  Next Obligation.
+  Proof.
+    unfold pointwise_relation in H.  
+    exists H0. apply H. assumption.
+  Qed.
+
+Program Instance {A : Type} => all_iff_morphism : 
+  Morphism (pointwise_relation iff ==> iff) (@all A).
+
+  Next Obligation.
+  Proof.
+    unfold pointwise_relation, all in *.
+    intuition ; specialize (H x0) ; intuition.
+  Qed.
+
+Program Instance {A : Type} => all_impl_morphism : 
+  Morphism (pointwise_relation impl ==> impl) (@all A).
+  
+  Next Obligation.
+  Proof.
+    unfold pointwise_relation, all in *.
+    intuition ; specialize (H x0) ; intuition.
+  Qed.
+
+Program Instance {A : Type} => all_inverse_impl_morphism : 
+  Morphism (pointwise_relation (inverse impl) ==> inverse impl) (@all A).
+  
+  Next Obligation.
+  Proof.
+    unfold pointwise_relation, all in *.
+    intuition ; specialize (H x0) ; intuition.
+  Qed.
diff --git a/theories/Classes/Morphisms_Relations.v b/theories/Classes/Morphisms_Relations.v
new file mode 100644
index 000000000..284810e94
--- /dev/null
+++ b/theories/Classes/Morphisms_Relations.v
@@ -0,0 +1,47 @@
+(* -*- coq-prog-args: ("-emacs-U" "-top" "Coq.Classes.Morphisms") -*- *)
+(************************************************************************)
+(*  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        *)
+(************************************************************************)
+
+(* Morphism instances for relations.
+ 
+   Author: Matthieu Sozeau
+   Institution: LRI, CNRS UMR 8623 - UniversitÃcopyright Paris Sud
+   91405 Orsay, France *)
+
+(** Morphisms for relations *)
+
+Instance relation_conjunction_morphism : Morphism (relation_equivalence (A:=A) ==>
+  relation_equivalence ==> relation_equivalence) relation_conjunction.
+  Proof. firstorder. Qed.
+
+Instance relation_disjunction_morphism : Morphism (relation_equivalence (A:=A) ==>
+  relation_equivalence ==> relation_equivalence) relation_disjunction.
+  Proof. firstorder. Qed.
+
+(* Predicate equivalence is exactly the same as the pointwise lifting of [iff]. *)
+
+Require Import List.
+
+Lemma predicate_equivalence_pointwise (l : list Type) :
+  Morphism (@predicate_equivalence l ==> lift_pointwise l iff) id.
+Proof. do 2 red. unfold predicate_equivalence. auto. Qed.
+
+Lemma predicate_implication_pointwise (l : list Type) :
+  Morphism (@predicate_implication l ==> lift_pointwise l impl) id.
+Proof. do 2 red. unfold predicate_implication. auto. Qed.
+
+(** The instanciation at relation allows to rewrite applications of relations [R x y] to [R' x y] *)
+(*    when [R] and [R'] are in [relation_equivalence]. *)
+
+Instance relation_equivalence_pointwise :
+  Morphism (relation_equivalence ==> pointwise_relation (A:=A) (pointwise_relation (A:=A) iff)) id.
+Proof. apply (predicate_equivalence_pointwise (l:=(cons A (cons A nil)))). Qed.
+
+Instance subrelation_pointwise :
+  Morphism (subrelation ==> pointwise_relation (A:=A) (pointwise_relation (A:=A) impl)) id.
+Proof. apply (predicate_implication_pointwise (l:=(cons A (cons A nil)))). Qed.
diff --git a/theories/Classes/RelationClasses.v b/theories/Classes/RelationClasses.v
index f5d3cc1c4..8dfb662b2 100644
--- a/theories/Classes/RelationClasses.v
+++ b/theories/Classes/RelationClasses.v
@@ -21,9 +21,6 @@ Require Import Coq.Program.Basics.
 Require Import Coq.Program.Tactics.
 Require Export Coq.Relations.Relation_Definitions.
 
-Set Implicit Arguments.
-Unset Strict Implicit.
-
 (** Default relation on a given support. *)
 
 Class DefaultRelation A (R : relation A).
@@ -50,6 +47,9 @@ Proof. reflexivity. Qed.
 
 (** We rebind relations in separate classes to be able to overload each proof. *)
 
+Set Implicit Arguments.
+Unset Strict Implicit.
+
 Class Reflexive A (R : relation A) :=
   reflexivity : forall x, R x x.
 
@@ -73,6 +73,8 @@ Implicit Arguments Transitive [A].
 
 Hint Resolve @irreflexivity : ord.
 
+Unset Implicit Arguments.
+
 (** We can already dualize all these properties. *)
 
 Program Instance [ Reflexive A R ] => flip_Reflexive : Reflexive (flip R) :=
@@ -115,12 +117,20 @@ Program Instance [ Symmetric A (R : relation A) ] => complement_Symmetric : Symm
 
 (** * Standard instances. *)
 
+Ltac reduce_hyp H :=
+  match type of H with
+    | context [ _ <-> _ ] => fail 1
+    | _ => red in H ; try reduce_hyp H
+  end.
+
 Ltac reduce_goal :=
   match goal with
     | [ |- _ <-> _ ] => fail 1
     | _ => red ; intros ; try reduce_goal
   end.
 
+Tactic Notation "reduce" "in" hyp(Hid) := reduce_hyp Hid.
+
 Ltac reduce := reduce_goal.
 
 Tactic Notation "apply" "*" constr(t) := 
@@ -203,52 +213,187 @@ Program Instance eq_equivalence : Equivalence A (@eq A) | 10.
 
 Program Instance iff_equivalence : Equivalence Prop iff.
 
-(** The following is not definable. *)
-(*
-Program Instance [ sa : Equivalence a R, sb : Equivalence b R' ] => equiv_setoid : 
-  Equivalence (a -> b)
-  (fun f g => forall (x y : a), R x y -> R' (f x) (g y)).
-*)
+(** We now develop a generalization of results on relations for arbitrary predicates.
+   The resulting theory can be applied to homogeneous binary relations but also to
+   arbitrary n-ary predicates. *)
 
+Require Import List.
 
-(** We define the various operations which define the algebra on relations.
-   They are essentially liftings of the logical operations. *)
+(* Notation " [ ] " := nil : list_scope. *)
+(* Notation " [ x ; .. ; y ] " := (cons x .. (cons y nil) ..) (at level 1) : list_scope. *)
 
-Definition relation_equivalence {A : Type} : relation (relation A) :=
-  fun (R R' : relation A) => forall x y, R x y <-> R' x y.
+(* Open Local Scope list_scope. *)
 
-Class subrelation {A:Type} (R R' : relation A) :=
-  is_subrelation : forall x y, R x y -> R' x y.
+(** A compact representation of non-dependent arities, with the codomain singled-out. *)
 
-Implicit Arguments subrelation [[A]].
+Fixpoint arrows (l : list Type) (r : Type) : Type := 
+  match l with 
+    | nil => r
+    | A :: l' => A -> arrows l' r
+  end.
 
+(** We can define abbreviations for operation and relation types based on [arrows]. *)
 
-Definition relation_conjunction {A} (R : relation A) (R' : relation A) : relation A :=
-  fun x y => R x y /\ R' x y.
+Definition unary_operation A := arrows (cons A nil) A.
+Definition binary_operation A := arrows (cons A (cons A nil)) A.
+Definition ternary_operation A := arrows (cons A (cons A (cons A nil))) A.
 
-Definition relation_disjunction {A} (R : relation A) (R' : relation A) : relation A :=
-  fun x y => R x y \/ R' x y.
+(** We define n-ary [predicate]s as functions into [Prop]. *)
 
-(* Infix "<R>" := relation_equivalence (at level 95, no associativity) : relation_scope. *)
-(* Infix "-R>" := subrelation (at level 70) : relation_scope. *)
-(* Infix "/R\" := relation_conjunction (at level 80, right associativity) : relation_scope. *)
-(* Infix "\R/" := relation_disjunction (at level 85, right associativity) : relation_scope. *)
+Definition predicate (l : list Type) := arrows l Prop.
 
-(* Open Local Scope relation_scope. *)
+(** Unary predicates, or sets. *)
 
-(** Relation equivalence is an equivalence, and subrelation defines a partial order. *)
+Definition unary_predicate A := predicate (cons A nil).
 
-Program Instance relation_equivalence_equivalence :
-  Equivalence (relation A) relation_equivalence.
+(** Homogenous binary relations, equivalent to [relation A]. *)
+
+Definition binary_relation A := predicate (cons A (cons A nil)).
+
+(** We can close a predicate by universal or existential quantification. *) 
+
+Fixpoint predicate_all (l : list Type) : predicate l -> Prop :=
+  match l with
+    | nil => fun f => f
+    | A :: tl => fun f => forall x : A, predicate_all tl (f x)
+  end.
+
+Fixpoint predicate_exists (l : list Type) : predicate l -> Prop :=
+  match l with
+    | nil => fun f => f
+    | A :: tl => fun f => exists x : A, predicate_exists tl (f x)
+  end.
+
+(** Pointwise extension of a binary operation on [T] to a binary operation 
+   on functions whose codomain is [T]. *)
+
+Fixpoint pointwise_extension {l : list Type} {T : Type}
+  (op : binary_operation T) : binary_operation (arrows l T) :=
+  match l with
+    | nil => fun R R' => op R R'
+    | A :: tl => fun R R' => 
+      fun x => pointwise_extension op (R x) (R' x)
+  end.
+
+(** For an operator on [Prop] this lifts the operator to a binary operation. *)
+
+Definition pointwise_relation_extension (l : list Type) (op : binary_relation Prop) : 
+  binary_operation (predicate l) := pointwise_extension op.
+
+(** Pointwise lifting, equivalent to doing [pointwise_extension] and closing using [predicate_all]. *)
+
+Fixpoint lift_pointwise (l : list Type) (op : binary_relation Prop) : binary_relation (predicate l) :=
+  match l with
+    | nil => fun R R' => op R R'
+    | A :: tl => fun R R' => 
+      forall x, lift_pointwise tl op (R x) (R' x)
+  end.
+
+(** The n-ary equivalence relation, defined by lifting the 0-ary [iff] relation. *)
+
+Definition predicate_equivalence {l : list Type} : binary_relation (predicate l) :=
+  lift_pointwise l iff.
+
+(** The n-ary implication relation, defined by lifting the 0-ary [impl] relation. *)
+
+Definition predicate_implication {l : list Type} :=
+  lift_pointwise l impl.
+
+(** Notations for pointwise equivalence and implication of predicates. *)
+
+Infix "<∙>" := predicate_equivalence (at level 95, no associativity) : predicate_scope.
+Infix "-∙>" := predicate_implication (at level 70) : predicate_scope.
+
+Open Local Scope predicate_scope.
+
+(** The pointwise liftings of conjunction and disjunctions.
+   Note that these are [binary_operation]s, building new relations out of old ones. *)
+
+Definition predicate_intersection {l : list Type} : binary_operation (predicate l) :=
+  pointwise_relation_extension l and.
+
+Definition predicate_union {l : list Type} : binary_operation (predicate l) :=
+  pointwise_relation_extension l or.
+
+Infix "/∙\" := predicate_intersection (at level 80, right associativity) : predicate_scope.
+Infix "\∙/" := predicate_union (at level 85, right associativity) : predicate_scope.
+
+(** The always [True] and always [False] predicates. *)
+
+Fixpoint true_predicate {l : list Type} : predicate l := 
+  match l with
+    | nil => True
+    | A :: tl => fun _ => @true_predicate tl
+  end.
+
+Fixpoint false_predicate {l : list Type} : predicate l :=
+  match l with
+    | nil => False
+    | A :: tl => fun _ => @false_predicate tl
+  end.
+
+Notation "∙⊤∙" := true_predicate : predicate_scope.
+Notation "∙⊥∙" := false_predicate : predicate_scope.
+
+(** Predicate equivalence is an equivalence, and predicate implication defines a preorder. *)
+
+Program Instance predicate_equivalence_equivalence :
+  Equivalence (predicate l) predicate_equivalence.
 
   Next Obligation.
-  Proof.
-    unfold relation_equivalence in *.
-    apply transitivity with (y x0 y0) ; [ apply H | apply H0 ].
+    induction l ; firstorder.
+  Qed.
+
+  Next Obligation.
+    induction l ; firstorder.
+  Qed.
+  
+  Next Obligation.
+    fold lift_pointwise.
+    induction l. firstorder.
+    intros. simpl in *. intro. pose (IHl (x x0) (y x0) (z x0)).
+    firstorder.
+  Qed.
+
+Program Instance predicate_implication_preorder :
+  PreOrder (predicate l) predicate_implication.
+
+  Next Obligation.
+    induction l ; firstorder.
   Qed.
 
-Program Instance subrelation_preorder :
-  PreOrder (relation A) subrelation.
+  Next Obligation.
+    fold lift_pointwise.
+    induction l. firstorder.
+    unfold predicate_implication in *. simpl in *. 
+    intro. pose (IHl (x x0) (y x0) (z x0)). firstorder.
+  Qed.
+
+(** We define the various operations which define the algebra on binary relations, 
+   from the general ones. *)
+
+Definition relation_equivalence {A : Type} : relation (relation A) :=
+  @predicate_equivalence (cons _ (cons _ nil)).
+
+Class subrelation {A:Type} (R R' : relation A) : Prop :=
+  is_subrelation : @predicate_implication (cons A (cons A nil)) R R'.
+
+Implicit Arguments subrelation [[A]].
+
+Definition relation_conjunction {A} (R : relation A) (R' : relation A) : relation A :=
+  @predicate_intersection (cons A (cons A nil)) R R'.
+
+Definition relation_disjunction {A} (R : relation A) (R' : relation A) : relation A :=
+  @predicate_union (cons A (cons A nil)) R R'.
+
+(** Relation equivalence is an equivalence, and subrelation defines a partial order. *)
+
+Instance (A : Type) => relation_equivalence_equivalence :
+  Equivalence (relation A) relation_equivalence.
+Proof. intro A. exact (@predicate_equivalence_equivalence (cons A (cons A nil))). Qed.
+
+Instance relation_implication_preorder : PreOrder (relation A) subrelation.
+Proof. intro A. exact (@predicate_implication_preorder (cons A (cons A nil))). Qed.
 
 (** *** Partial Order.
    A partial order is a preorder which is additionally antisymmetric.
@@ -256,8 +401,7 @@ Program Instance subrelation_preorder :
    on the carrier. *)
 
 Class [ equ : Equivalence A eqA, PreOrder A R ] => PartialOrder :=
-  partial_order_equivalence : relation_equivalence eqA (relation_conjunction R (flip R)).
-
+  partial_order_equivalence : relation_equivalence eqA (relation_conjunction R (inverse R)).
 
 (** The equivalence proof is sufficient for proving that [R] must be a morphism 
    for equivalence (see Morphisms).
@@ -265,8 +409,8 @@ Class [ equ : Equivalence A eqA, PreOrder A R ] => PartialOrder :=
 
 Instance [ PartialOrder A eqA R ] =>  partial_order_antisym : ! Antisymmetric A eqA R.
 Proof with auto.
-  reduce_goal. pose partial_order_equivalence. red in r.
-  apply <- r. firstorder.
+  reduce_goal. pose partial_order_equivalence as poe. do 3 red in poe. 
+  apply <- poe. firstorder.
 Qed.
 
 (** The partial order defined by subrelation and relation equivalence. *)
@@ -279,8 +423,6 @@ Program Instance subrelation_partial_order :
     unfold relation_equivalence in *. firstorder.
   Qed.
 
-Instance iff_impl_subrelation : subrelation iff impl.
-Proof. firstorder. Qed.
-
-Instance iff_inverse_impl_subrelation : subrelation iff (inverse impl).
-Proof. firstorder. Qed.
+Lemma inverse_pointwise_relation A (R : relation A) : 
+  relation_equivalence (pointwise_relation (inverse R)) (inverse (pointwise_relation (A:=A) R)).
+Proof. reflexivity. Qed.
diff --git a/theories/Classes/SetoidTactics.v b/theories/Classes/SetoidTactics.v
index 38bdc0bc9..9d3648fef 100644
--- a/theories/Classes/SetoidTactics.v
+++ b/theories/Classes/SetoidTactics.v
@@ -17,6 +17,7 @@
 
 Require Export Coq.Classes.RelationClasses.
 Require Export Coq.Classes.Morphisms.
+Require Export Coq.Classes.Morphisms_Prop.
 Require Export Coq.Classes.Equivalence.
 Require Export Coq.Relations.Relation_Definitions.
 
@@ -89,6 +90,7 @@ Ltac reverse_arrows x :=
   end.
 
 Ltac default_add_morphism_tactic :=
+  intros ;
   (try destruct_morphism) ;
   match goal with
     | [ |- (?x ==> ?y) _ _ ] => red_subst_eq_morphism (x ==> y) ; reverse_arrows (x ==> y)
diff --git a/theories/FSets/FMapFacts.v b/theories/FSets/FMapFacts.v
index 6d77a6a0c..617ea6f4f 100644
--- a/theories/FSets/FMapFacts.v
+++ b/theories/FSets/FMapFacts.v
@@ -651,7 +651,7 @@ Proof. unfold Equal; congruence. Qed.
 
 Definition Equal_ST : forall elt:Type, Setoid_Theory (t elt) (@Equal _).
 Proof. 
-constructor; [apply Equal_refl | apply Equal_sym | apply Equal_trans].
+constructor; red; [apply Equal_refl | apply Equal_sym | apply Equal_trans].
 Qed.
 
 Add Relation key E.eq 
diff --git a/theories/FSets/FSetFacts.v b/theories/FSets/FSetFacts.v
index 0c19176f8..6afb8fcb7 100644
--- a/theories/FSets/FSetFacts.v
+++ b/theories/FSets/FSetFacts.v
@@ -295,12 +295,12 @@ End BoolSpec.
 
 Definition E_ST : Setoid_Theory elt E.eq.
 Proof.
-constructor; [apply E.eq_refl|apply E.eq_sym|apply E.eq_trans].
+constructor ; red; [apply E.eq_refl|apply E.eq_sym|apply E.eq_trans].
 Qed.
 
 Definition Equal_ST : Setoid_Theory t Equal.
 Proof. 
-constructor; [apply eq_refl | apply eq_sym | apply eq_trans].
+constructor ; red; [apply eq_refl | apply eq_sym | apply eq_trans].
 Qed.
 
 Add Relation elt E.eq 
diff --git a/theories/Lists/List.v b/theories/Lists/List.v
index 6b30f6351..5ab27cfc7 100644
--- a/theories/Lists/List.v
+++ b/theories/Lists/List.v
@@ -9,7 +9,6 @@
   (*i $Id$ i*)
 
 Require Import Le Gt Minus Min Bool.
-Require Import Coq.Setoids.Setoid.
 
 Set Implicit Arguments.
 
@@ -554,8 +553,7 @@ Section Elts.
     simpl; intros; split; [destruct 1 | apply gt_irrefl].
     simpl. intro x; destruct (eqA_dec y x) as [Heq|Hneq].
     rewrite Heq; intuition. 
-    rewrite <- (IHl x).
-    tauto.
+    pose (IHl x). intuition.
   Qed.
   
   Theorem count_occ_inv_nil : forall (l : list A), (forall x:A, count_occ l x = 0) <-> l = nil.
diff --git a/theories/Program/Syntax.v b/theories/Program/Syntax.v
index a518faa57..6158e88f7 100644
--- a/theories/Program/Syntax.v
+++ b/theories/Program/Syntax.v
@@ -44,7 +44,7 @@ Implicit Arguments cons [[A]].
 
 Notation " [] " := nil.
 Notation " [ x ] " := (cons x nil).
-Notation " [ x ; .. ; y ] " := (cons x .. (cons y nil) ..).
+Notation " [ x ; .. ; y ] " := (cons x .. (cons y nil) ..) (at level 1).
 
 (** n-ary exists ! *)
 
diff --git a/theories/QArith/QArith_base.v b/theories/QArith/QArith_base.v
index 26638893a..2265715b7 100644
--- a/theories/QArith/QArith_base.v
+++ b/theories/QArith/QArith_base.v
@@ -121,7 +121,7 @@ Defined.
 
 Definition Q_Setoid : Setoid_Theory Q Qeq.
 Proof.
- split; unfold Qeq in |- *; auto; apply Qeq_trans.
+ split; red; unfold Qeq in |- *; auto; apply Qeq_trans.
 Qed.
 
 Add Setoid Q Qeq Q_Setoid as Qsetoid.
diff --git a/theories/Setoids/Setoid.v b/theories/Setoids/Setoid.v
index 983c651ab..8f59c048f 100644
--- a/theories/Setoids/Setoid.v
+++ b/theories/Setoids/Setoid.v
@@ -8,22 +8,18 @@
 
 (*i $Id$: i*)
 
-Set Implicit Arguments.
-
 Require Export Coq.Classes.SetoidTactics.
 
 (** For backward compatibility *)
 
-Record Setoid_Theory  (A: Type) (Aeq: relation A) : 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 }.
-
-Implicit Arguments Setoid_Theory [].
-Implicit Arguments Seq_refl [].
-Implicit Arguments Seq_sym [].
-Implicit Arguments Seq_trans [].
-
+Definition Setoid_Theory := @Equivalence.  
+Definition Build_Setoid_Theory := @Build_Equivalence.  
+Definition Seq_refl A Aeq (s : Setoid_Theory A Aeq) : forall x:A, Aeq x x :=
+  Eval compute in reflexivity.
+Definition Seq_sym A Aeq (s : Setoid_Theory A Aeq) : forall x y:A, Aeq x y -> Aeq y x :=
+  Eval compute in symmetry.
+Definition Seq_trans A Aeq (s : Setoid_Theory A Aeq) : forall x y z:A, Aeq x y -> Aeq y z -> Aeq x z :=
+  Eval compute in transitivity.
 
 (** Some tactics for manipulating Setoid Theory not officially 
     declared as Setoid. *)
diff --git a/toplevel/classes.ml b/toplevel/classes.ml
index bc627a283..203fe118d 100644
--- a/toplevel/classes.ml
+++ b/toplevel/classes.ml
@@ -552,8 +552,9 @@ let new_instance ctx (instid, bk, cl) props ?(tac:Proof_type.tactic option) ?(ho
 	    let kind = Decl_kinds.Global, Decl_kinds.DefinitionBody Decl_kinds.Instance in
 	      Flags.silently (fun () ->
 		Command.start_proof id kind termtype (fun _ -> function ConstRef cst -> hook cst | _ -> assert false);
-		Pfedit.by (* (Refiner.tclTHEN (Refiner.tclEVARS (Evd.evars_of !isevars)) *)
-		  (!refine_ref (evm, term));
+		if props <> [] then 
+		  Pfedit.by (* (Refiner.tclTHEN (Refiner.tclEVARS (Evd.evars_of !isevars)) *)
+		    (!refine_ref (evm, term));
 		(match tac with Some tac -> Pfedit.by tac | None -> ())) ();
 	      Flags.if_verbose (msg $$ Printer.pr_open_subgoals) ();
 	      id