Imported Upstream snapshot 8.3~beta0+13298

14 files changed, 760 insertions, 485 deletions

diff --git a/theories/Classes/EquivDec.v b/theories/Classes/EquivDec.v
index 15cabf81..0a35ef45 100644
--- a/theories/Classes/EquivDec.v
+++ b/theories/Classes/EquivDec.v
@@ -6,46 +6,51 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* Decidable equivalences.
- *
- * Author: Matthieu Sozeau
- * Institution: LRI, CNRS UMR 8623 - Universit脙copyright Paris Sud
- *              91405 Orsay, France *)
+(** * Decidable equivalences.
 
-(* $Id: EquivDec.v 12187 2009-06-13 19:36:59Z msozeau $ *)
+   Author: Matthieu Sozeau
+   Institution: LRI, CNRS UMR 8623 - University Paris Sud
+*)
+
+(* $Id$ *)
 
 (** Export notations. *)
 
 Require Export Coq.Classes.Equivalence.
 
-(** The [DecidableSetoid] class asserts decidability of a [Setoid]. It can be useful in proofs to reason more 
-   classically. *)
+(** The [DecidableSetoid] class asserts decidability of a [Setoid].
+   It can be useful in proofs to reason more classically. *)
 
 Require Import Coq.Logic.Decidable.
+Require Import Coq.Bool.Bool.
+Require Import Coq.Arith.Peano_dec.
+Require Import Coq.Program.Program.
+
+Generalizable Variables A B R.
 
 Open Scope equiv_scope.
 
 Class DecidableEquivalence `(equiv : Equivalence A) :=
   setoid_decidable : forall x y : A, decidable (x === y).
 
-(** The [EqDec] class gives a decision procedure for a particular setoid equality. *)
+(** The [EqDec] class gives a decision procedure for a particular
+   setoid equality. *)
 
 Class EqDec A R {equiv : Equivalence R} :=
   equiv_dec : forall x y : A, { x === y } + { x =/= y }.
 
-(** We define the [==] overloaded notation for deciding equality. It does not take precedence
-   of [==] defined in the type scope, hence we can have both at the same time. *)
+(** We define the [==] overloaded notation for deciding equality. It does not
+   take precedence of [==] defined in the type scope, hence we can have both
+   at the same time. *)
 
 Notation " x == y " := (equiv_dec (x :>) (y :>)) (no associativity, at level 70) : equiv_scope.
 
 Definition swap_sumbool {A B} (x : { A } + { B }) : { B } + { A } :=
   match x with
-    | left H => @right _ _ H 
-    | right H => @left _ _ H 
+    | left H => @right _ _ H
+    | right H => @left _ _ H
   end.
 
-Require Import Coq.Program.Program.
-
 Open Local Scope program_scope.
 
 (** Invert the branches. *)
@@ -69,17 +74,14 @@ Infix "<>b" := nequiv_decb (no associativity, at level 70).
 
 (** Decidable leibniz equality instances. *)
 
-Require Import Coq.Arith.Peano_dec.
-
-(** The equiv is burried inside the setoid, but we can recover it by specifying which setoid we're talking about. *)
+(** The equiv is burried inside the setoid, but we can recover it by specifying
+   which setoid we're talking about. *)
 
 Program Instance nat_eq_eqdec : EqDec nat eq := eq_nat_dec.
 
-Require Import Coq.Bool.Bool.
-
 Program Instance bool_eqdec : EqDec bool eq := bool_dec.
 
-Program Instance unit_eqdec : EqDec unit eq := 位 x y, in_left.
+Program Instance unit_eqdec : EqDec unit eq := fun x y => in_left.
 
   Next Obligation.
   Proof.
@@ -87,41 +89,37 @@ Program Instance unit_eqdec : EqDec unit eq := 位 x y, in_left.
     reflexivity.
   Qed.
 
+Obligation Tactic := unfold complement, equiv ; program_simpl.
+
 Program Instance prod_eqdec `(EqDec A eq, EqDec B eq) :
   ! EqDec (prod A B) eq :=
   { equiv_dec x y :=
-    let '(x1, x2) := x in 
-    let '(y1, y2) := y in 
-    if x1 == y1 then 
+    let '(x1, x2) := x in
+    let '(y1, y2) := y in
+    if x1 == y1 then
       if x2 == y2 then in_left
       else in_right
     else in_right }.
 
-  Solve Obligations using unfold complement, equiv ; program_simpl.
-
 Program Instance sum_eqdec `(EqDec A eq, EqDec B eq) :
   EqDec (sum A B) eq := {
-  equiv_dec x y := 
+  equiv_dec x y :=
     match x, y with
       | inl a, inl b => if a == b then in_left else in_right
       | inr a, inr b => if a == b then in_left else in_right
       | inl _, inr _ | inr _, inl _ => in_right
     end }.
 
-  Solve Obligations using unfold complement, equiv ; program_simpl.
-
-(** Objects of function spaces with countable domains like bool have decidable equality. 
-   Proving the reflection requires functional extensionality though. *)
+(** Objects of function spaces with countable domains like bool have decidable
+  equality. Proving the reflection requires functional extensionality though. *)
 
 Program Instance bool_function_eqdec `(EqDec A eq) : ! EqDec (bool -> A) eq :=
-  { equiv_dec f g := 
+  { equiv_dec f g :=
     if f true == g true then
       if f false == g false then in_left
       else in_right
     else in_right }.
 
-  Solve Obligations using try red ; unfold equiv, complement ; program_simpl.
-
   Next Obligation.
   Proof.
     extensionality x.
@@ -131,21 +129,19 @@ Program Instance bool_function_eqdec `(EqDec A eq) : ! EqDec (bool -> A) eq :=
 Require Import List.
 
 Program Instance list_eqdec `(eqa : EqDec A eq) : ! EqDec (list A) eq :=
-  { equiv_dec := 
-    fix aux (x : list A) y { struct x } :=
+  { equiv_dec :=
+    fix aux (x y : list A) :=
     match x, y with
       | nil, nil => in_left
-      | cons hd tl, cons hd' tl' => 
+      | cons hd tl, cons hd' tl' =>
         if hd == hd' then
           if aux tl tl' then in_left else in_right
           else in_right
       | _, _ => in_right
     end }.
 
-  Solve Obligations using unfold equiv, complement in *; program_simpl;
-    intuition (discriminate || eauto).
+  Solve Obligations using unfold equiv, complement in * ; program_simpl ; intuition (discriminate || eauto).
 
-  Next Obligation. destruct x ; destruct y ; intuition eauto. Defined.
+  Next Obligation. destruct y ; intuition eauto. Defined.
 
-  Solve Obligations using unfold equiv, complement in *; program_simpl;
-    intuition (discriminate || eauto).
+  Solve Obligations using unfold equiv, complement in * ; program_simpl ; intuition (discriminate || eauto).
diff --git a/theories/Classes/Equivalence.v b/theories/Classes/Equivalence.v
index 7068bc6b..d0f24347 100644
--- a/theories/Classes/Equivalence.v
+++ b/theories/Classes/Equivalence.v
@@ -6,13 +6,13 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* Typeclass-based setoids. Definitions on [Equivalence].
- 
+(** * Typeclass-based setoids. Definitions on [Equivalence].
+
    Author: Matthieu Sozeau
-   Institution: LRI, CNRS UMR 8623 - Universit胏opyright Paris Sud
-   91405 Orsay, France *) 
+   Institution: LRI, CNRS UMR 8623 - University Paris Sud
+*)
 
-(* $Id: Equivalence.v 12187 2009-06-13 19:36:59Z msozeau $ *)
+(* $Id$ *)
 
 Require Import Coq.Program.Basics.
 Require Import Coq.Program.Tactics.
@@ -25,16 +25,20 @@ Require Import Coq.Classes.Morphisms.
 Set Implicit Arguments.
 Unset Strict Implicit.
 
+Generalizable Variables A R eqA B S eqB.
+Local Obligation Tactic := simpl_relation.
+
 Open Local Scope signature_scope.
 
 Definition equiv `{Equivalence A R} : relation A := R.
 
-(** Overloaded notations for setoid equivalence and inequivalence. Not to be confused with [eq] and [=]. *)
+(** Overloaded notations for setoid equivalence and inequivalence.
+    Not to be confused with [eq] and [=]. *)
 
 Notation " x === y " := (equiv x y) (at level 70, no associativity) : equiv_scope.
 
 Notation " x =/= y " := (complement equiv x y) (at level 70, no associativity) : equiv_scope.
-  
+
 Open Local Scope equiv_scope.
 
 (** Overloading for [PER]. *)
@@ -60,7 +64,7 @@ Program Instance equiv_transitive `(sa : Equivalence A) : Transitive equiv.
 
 (** Use the [substitute] command which substitutes an equivalence in every hypothesis. *)
 
-Ltac setoid_subst H := 
+Ltac setoid_subst H :=
   match type of H with
     ?x === ?y => substitute H ; clear H x
   end.
@@ -70,7 +74,7 @@ Ltac setoid_subst_nofail :=
     | [ 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.
@@ -100,19 +104,19 @@ Ltac equivify := repeat equivify_tac.
 
 Section Respecting.
 
-  (** Here we build an equivalence instance for functions which relates respectful ones only, 
+  (** Here we build an equivalence instance for functions which relates respectful ones only,
      we do not export it. *)
 
-  Definition respecting `(eqa : Equivalence A (R : relation A), eqb : Equivalence B (R' : relation B)) : Type := 
+  Definition respecting `(eqa : Equivalence A (R : relation A), eqb : Equivalence B (R' : relation B)) : Type :=
     { morph : A -> B | respectful R R' morph morph }.
-  
+
   Program Instance respecting_equiv `(eqa : Equivalence A R, eqb : Equivalence B R') :
     Equivalence (fun (f g : respecting eqa eqb) => 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. 
+  Proof.
     unfold respecting in *. program_simpl. transitivity (y y0); auto. apply H0. reflexivity.
   Qed.
 
diff --git a/theories/Classes/Functions.v b/theories/Classes/Functions.v
deleted file mode 100644
index 998f8cb7..00000000
--- a/theories/Classes/Functions.v
+++ /dev/null
@@ -1,41 +0,0 @@
-(************************************************************************)
-(*  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        *)
-(************************************************************************)
-
-(* Functional morphisms.
- 
-   Author: Matthieu Sozeau
-   Institution: LRI, CNRS UMR 8623 - Universit脙copyright Paris Sud
-   91405 Orsay, France *)
-
-(* $Id: Functions.v 11709 2008-12-20 11:42:15Z msozeau $ *)
-
-Require Import Coq.Classes.RelationClasses.
-Require Import Coq.Classes.Morphisms.
-
-Set Implicit Arguments.
-Unset Strict Implicit.
-
-Class Injective `(m : Morphism (A -> B) (RA ++> RB) f) : Prop :=
-  injective : forall x y : A, RB (f x) (f y) -> RA x y.
-
-Class Surjective `(m : Morphism (A -> B) (RA ++> RB) f) : Prop :=
-  surjective : forall y, exists x : A, RB y (f x).
-
-Definition Bijective `(m : Morphism (A -> B) (RA ++> RB) (f : A -> B)) :=
-  Injective m /\ Surjective m.
-
-Class MonoMorphism `(m : Morphism (A -> B) (eqA ++> eqB)) :=
-  monic :> Injective m.
-
-Class EpiMorphism `(m : Morphism (A -> B) (eqA ++> eqB)) :=
-  epic :> Surjective m.
-
-Class IsoMorphism `(m : Morphism (A -> B) (eqA ++> eqB)) :=
-  { monomorphism :> MonoMorphism m ; epimorphism :> EpiMorphism m }.
-
-Class AutoMorphism `(m : Morphism (A -> A) (eqA ++> eqA)) {I : IsoMorphism m}.
diff --git a/theories/Classes/Init.v b/theories/Classes/Init.v
index 762cc5c1..f6e51018 100644
--- a/theories/Classes/Init.v
+++ b/theories/Classes/Init.v
@@ -6,22 +6,26 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* Initialization code for typeclasses, setting up the default tactic 
+(** * Initialization code for typeclasses, setting up the default tactic
    for instance search.
 
    Author: Matthieu Sozeau
-   Institution: LRI, CNRS UMR 8623 - Universit脙copyright Paris Sud
-   91405 Orsay, France *)
+   Institution: LRI, CNRS UMR 8623 - University Paris Sud
+*)
 
-(* $Id: Init.v 12187 2009-06-13 19:36:59Z msozeau $ *)
+(* $Id$ *)
 
 (** Hints for the proof search: these combinators should be considered rigid. *)
 
 Require Import Coq.Program.Basics.
 
-Typeclasses Opaque id const flip compose arrow impl iff.
+Typeclasses Opaque id const flip compose arrow impl iff not all.
 
-(** The unconvertible typeclass, to test that two objects of the same type are 
+(** Apply using the same opacity information as typeclass proof search. *)
+
+Ltac class_apply c := autoapply c using typeclass_instances.
+
+(** The unconvertible typeclass, to test that two objects of the same type are
    actually different. *)
 
 Class Unconvertible (A : Type) (a b : A) := unconvertible : unit.
diff --git a/theories/Classes/Morphisms.v b/theories/Classes/Morphisms.v
index 2b653e27..370321c0 100644
--- a/theories/Classes/Morphisms.v
+++ b/theories/Classes/Morphisms.v
@@ -1,3 +1,4 @@
+(* -*- coding: utf-8 -*- *)
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
 (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
@@ -6,41 +7,44 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* Typeclass-based morphism definition and standard, minimal instances.
- 
+(** * Typeclass-based morphism definition and standard, minimal instances
+
    Author: Matthieu Sozeau
-   Institution: LRI, CNRS UMR 8623 - Universit脙copyright Paris Sud
-   91405 Orsay, France *)
+   Institution: LRI, CNRS UMR 8623 - University Paris Sud
+*)
 
-(* $Id: Morphisms.v 12189 2009-06-15 05:08:44Z msozeau $ *)
+(* $Id$ *)
 
 Require Import Coq.Program.Basics.
 Require Import Coq.Program.Tactics.
 Require Import Coq.Relations.Relation_Definitions.
 Require Export Coq.Classes.RelationClasses.
 
+Generalizable All Variables.
+Local Obligation Tactic := simpl_relation.
+
 (** * Morphisms.
 
-   We now turn to the definition of [Morphism] and declare standard instances. 
+   We now turn to the definition of [Proper] and declare standard instances.
    These will be used by the [setoid_rewrite] tactic later. *)
 
-(** 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. *)
+(** A morphism for a relation [R] is a proper element of the relation.
+   The relation [R] will be instantiated by [respectful] and [A] by an arrow
+   type for usual morphisms. *)
 
-Class Morphism {A} (R : relation A) (m : A) : Prop :=
-  respect : R m m.
+Class Proper {A} (R : relation A) (m : A) : Prop :=
+  proper_prf : R m m.
 
 (** Respectful morphisms. *)
 
 (** The fully dependent version, not used yet. *)
 
-Definition respectful_hetero 
-  (A B : Type) 
-  (C : A -> Type) (D : B -> Type) 
-  (R : A -> B -> Prop) 
-  (R' : forall (x : A) (y : B), C x -> D y -> Prop) : 
-    (forall x : A, C x) -> (forall x : B, D x) -> Prop := 
+Definition respectful_hetero
+  (A B : Type)
+  (C : A -> Type) (D : B -> Type)
+  (R : A -> B -> Prop)
+  (R' : forall (x : A) (y : B), C x -> D y -> Prop) :
+    (forall x : A, C x) -> (forall x : B, D x) -> Prop :=
     fun f g => forall x y, R x y -> R' x y (f x) (g y).
 
 (** The non-dependent version is an instance where we forget dependencies. *)
@@ -53,27 +57,27 @@ Definition respectful {A B : Type}
 
 Delimit Scope signature_scope with signature.
 
-Arguments Scope Morphism [type_scope signature_scope].
+Arguments Scope Proper [type_scope signature_scope].
 Arguments Scope respectful [type_scope type_scope signature_scope signature_scope].
 
-Module MorphismNotations.
+Module ProperNotations.
 
-  Notation " R ++> R' " := (@respectful _ _ (R%signature) (R'%signature)) 
+  Notation " R ++> R' " := (@respectful _ _ (R%signature) (R'%signature))
     (right associativity, at level 55) : signature_scope.
-  
+
   Notation " R ==> R' " := (@respectful _ _ (R%signature) (R'%signature))
     (right associativity, at level 55) : signature_scope.
-  
+
   Notation " R --> R' " := (@respectful _ _ (inverse (R%signature)) (R'%signature))
     (right associativity, at level 55) : signature_scope.
 
-End MorphismNotations.
+End ProperNotations.
 
-Export MorphismNotations.
+Export ProperNotations.
 
 Open Local Scope signature_scope.
 
-(** Dependent pointwise lifting of a relation on the range. *) 
+(** Dependent pointwise lifting of a relation on the range. *)
 
 Definition forall_relation {A : Type} {B : A -> Type} (sig : 螤 a : A, relation (B a)) : relation (螤 x : A, B x) :=
   位 f g, 螤 a : A, sig a (f a) (g a).
@@ -82,10 +86,10 @@ Arguments Scope forall_relation [type_scope type_scope signature_scope].
 
 (** Non-dependent pointwise lifting *)
 
-Definition pointwise_relation (A : Type) {B : Type} (R : relation B) : relation (A -> B) := 
+Definition pointwise_relation (A : Type) {B : Type} (R : relation B) : relation (A -> B) :=
   Eval compute in forall_relation (B:=位 _, B) (位 _, R).
 
-Lemma pointwise_pointwise A B (R : relation B) : 
+Lemma pointwise_pointwise A B (R : relation B) :
   relation_equivalence (pointwise_relation A R) (@eq A ==> R).
 Proof. intros. split. simpl_relation. firstorder. Qed.
 
@@ -98,8 +102,7 @@ Hint Unfold Transitive : core.
 
 Typeclasses Opaque respectful pointwise_relation forall_relation.
 
-Program Instance respectful_per `(PER A (R : relation A), PER B (R' : relation B)) : 
-  PER (R ==> R').
+Program Instance respectful_per `(PER A R, PER B R') : PER (R ==> R').
 
   Next Obligation.
   Proof with auto.
@@ -110,47 +113,46 @@ Program Instance respectful_per `(PER A (R : relation A), PER B (R' : relation B
 
 (** Subrelations induce a morphism on the identity. *)
 
-Instance subrelation_id_morphism `(subrelation A R鈧� R鈧�) : Morphism (R鈧� ==> R鈧�) id.
+Instance subrelation_id_proper `(subrelation A R鈧� R鈧�) : Proper (R鈧� ==> R鈧�) id.
 Proof. firstorder. Qed.
 
 (** The subrelation property goes through products as usual. *)
 
-Instance morphisms_subrelation_respectful `(subl : subrelation A R鈧� R鈧�, subr : subrelation B S鈧� S鈧�) :
+Lemma subrelation_respectful `(subl : subrelation A R鈧� R鈧�, subr : subrelation B S鈧� S鈧�) :
   subrelation (R鈧� ==> S鈧�) (R鈧� ==> S鈧�).
 Proof. simpl_relation. apply subr. apply H. apply subl. apply H0. Qed.
 
 (** And of course it is reflexive. *)
 
-Instance morphisms_subrelation_refl : ! subrelation A R R.
+Lemma subrelation_refl A R : @subrelation A R R.
 Proof. simpl_relation. Qed.
 
-(** [Morphism] is itself a covariant morphism for [subrelation]. *)
+Ltac subrelation_tac T U :=
+  (is_ground T ; is_ground U ; class_apply @subrelation_refl) ||
+    class_apply @subrelation_respectful || class_apply @subrelation_refl.
+
+Hint Extern 3 (@subrelation _ ?T ?U) => subrelation_tac T U : typeclass_instances.
 
-Lemma subrelation_morphism `(mor : Morphism A R鈧� m, unc : Unconvertible (relation A) R鈧� R鈧�,
-  sub : subrelation A R鈧� R鈧�) : Morphism R鈧� m.
+(** [Proper] is itself a covariant morphism for [subrelation]. *)
+
+Lemma subrelation_proper `(mor : Proper A R鈧� m, unc : Unconvertible (relation A) R鈧� R鈧�,
+  sub : subrelation A R鈧� R鈧�) : Proper R鈧� m.
 Proof.
   intros. apply sub. apply mor.
 Qed.
 
-Instance morphism_subrelation_morphism : 
-  Morphism (subrelation ++> @eq _ ==> impl) (@Morphism A).
-Proof. reduce. subst. firstorder. Qed.
-
-(** 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.
+CoInductive apply_subrelation : Prop := do_subrelation.
 
-Inductive normalization_done : Prop := did_normalization.
-
-Ltac subrelation_tac := 
+Ltac proper_subrelation :=
   match goal with
-    | [ _ : subrelation_done |- _ ] => fail 1
-    | [ |- @Morphism _ _ _ ] => let H := fresh "H" in
-      set(H:=did_subrelation) ; eapply @subrelation_morphism
+    [ H : apply_subrelation |- _ ] => clear H ; class_apply @subrelation_proper
   end.
 
-Hint Extern 5 (@Morphism _ _ _) => subrelation_tac : typeclass_instances.
+Hint Extern 5 (@Proper _ ?H _) => proper_subrelation : typeclass_instances.
+
+Instance proper_subrelation_proper :
+  Proper (subrelation ++> eq ==> impl) (@Proper A).
+Proof. reduce. subst. firstorder. Qed.
 
 (** Essential subrelation instances for [iff], [impl] and [pointwise_relation]. *)
 
@@ -164,11 +166,29 @@ Instance pointwise_subrelation {A} `(sub : subrelation B R R') :
   subrelation (pointwise_relation A R) (pointwise_relation A R') | 4.
 Proof. reduce. unfold pointwise_relation in *. apply sub. apply H. Qed.
 
-(** The complement of a relation conserves its morphisms. *)
+(** For dependent function types. *)
+Lemma forall_subrelation A (B : A -> Type) (R S : forall x : A, relation (B x)) :
+  (forall a, subrelation (R a) (S a)) -> subrelation (forall_relation R) (forall_relation S).
+Proof. reduce. apply H. apply H0. Qed.
+
+(** We use an extern hint to help unification. *)
+
+Hint Extern 4 (subrelation (@forall_relation ?A ?B ?R) (@forall_relation _ _ ?S)) =>
+  apply (@forall_subrelation A B R S) ; intro : typeclass_instances.
+
+(** Any symmetric relation is equal to its inverse. *)
+
+Lemma subrelation_symmetric A R `(Symmetric A R) : subrelation (inverse R) R.
+Proof. reduce. red in H0. symmetry. assumption. Qed.
+
+Hint Extern 4 (subrelation (inverse _) _) => 
+  class_apply @subrelation_symmetric : typeclass_instances.
 
-Program Instance complement_morphism
-  `(mR : Morphism (A -> A -> Prop) (RA ==> RA ==> iff) R) :
-  Morphism (RA ==> RA ==> iff) (complement R).
+(** The complement of a relation conserves its proper elements. *)
+
+Program Instance complement_proper
+  `(mR : Proper (A -> A -> Prop) (RA ==> RA ==> iff) R) :
+  Proper (RA ==> RA ==> iff) (complement R).
 
   Next Obligation.
   Proof.
@@ -177,22 +197,22 @@ Program Instance complement_morphism
     intuition.
   Qed.
 
-(** The [inverse] too, actually the [flip] instance is a bit more general. *) 
+(** The [inverse] too, actually the [flip] instance is a bit more general. *)
 
-Program Instance flip_morphism
-  `(mor : Morphism (A -> B -> C) (RA ==> RB ==> RC) f) :
-  Morphism (RB ==> RA ==> RC) (flip f).
+Program Instance flip_proper
+  `(mor : Proper (A -> B -> C) (RA ==> RB ==> RC) f) :
+  Proper (RB ==> RA ==> RC) (flip f).
 
   Next Obligation.
   Proof.
     apply mor ; auto.
   Qed.
 
-(** Every Transitive relation gives rise to a binary morphism on [impl], 
+(** Every Transitive relation gives rise to a binary morphism on [impl],
    contravariant in the first argument, covariant in the second. *)
 
 Program Instance trans_contra_co_morphism
-  `(Transitive A R) : Morphism (R --> R ++> impl) R.
+  `(Transitive A R) : Proper (R --> R ++> impl) R.
 
   Next Obligation.
   Proof with auto.
@@ -200,10 +220,10 @@ Program Instance trans_contra_co_morphism
     transitivity x0...
   Qed.
 
-(** Morphism declarations for partial applications. *)
+(** Proper declarations for partial applications. *)
 
 Program Instance trans_contra_inv_impl_morphism
-  `(Transitive A R) : Morphism (R --> inverse impl) (R x) | 3.
+  `(Transitive A R) : Proper (R --> inverse impl) (R x) | 3.
 
   Next Obligation.
   Proof with auto.
@@ -211,7 +231,7 @@ Program Instance trans_contra_inv_impl_morphism
   Qed.
 
 Program Instance trans_co_impl_morphism
-  `(Transitive A R) : Morphism (R ==> impl) (R x) | 3.
+  `(Transitive A R) : Proper (R ++> impl) (R x) | 3.
 
   Next Obligation.
   Proof with auto.
@@ -219,7 +239,7 @@ Program Instance trans_co_impl_morphism
   Qed.
 
 Program Instance trans_sym_co_inv_impl_morphism
-  `(PER A R) : Morphism (R ==> inverse impl) (R x) | 2.
+  `(PER A R) : Proper (R ++> inverse impl) (R x) | 3.
 
   Next Obligation.
   Proof with auto.
@@ -227,7 +247,7 @@ Program Instance trans_sym_co_inv_impl_morphism
   Qed.
 
 Program Instance trans_sym_contra_impl_morphism
-  `(PER A R) : Morphism (R --> impl) (R x) | 2.
+  `(PER A R) : Proper (R --> impl) (R x) | 3.
 
   Next Obligation.
   Proof with auto.
@@ -235,7 +255,7 @@ Program Instance trans_sym_contra_impl_morphism
   Qed.
 
 Program Instance per_partial_app_morphism
-  `(PER A R) : Morphism (R ==> iff) (R x) | 1.
+  `(PER A R) : Proper (R ==> iff) (R x) | 2.
 
   Next Obligation.
   Proof with auto.
@@ -249,7 +269,7 @@ Program Instance per_partial_app_morphism
    to get an [R y z] goal. *)
 
 Program Instance trans_co_eq_inv_impl_morphism
-  `(Transitive A R) : Morphism (R ==> (@eq A) ==> inverse impl) R | 2.
+  `(Transitive A R) : Proper (R ==> (@eq A) ==> inverse impl) R | 2.
 
   Next Obligation.
   Proof with auto.
@@ -258,21 +278,21 @@ Program Instance trans_co_eq_inv_impl_morphism
 
 (** Every Symmetric and Transitive relation gives rise to an equivariant morphism. *)
 
-Program Instance PER_morphism `(PER A R) : Morphism (R ==> R ==> iff) R | 1.
+Program Instance PER_morphism `(PER A R) : Proper (R ==> R ==> iff) R | 1.
 
   Next Obligation.
   Proof with auto.
     split ; intros.
     transitivity x0... transitivity x... symmetry...
-  
+
     transitivity y... transitivity y0... symmetry...
   Qed.
 
 Lemma symmetric_equiv_inverse `(Symmetric A R) : relation_equivalence R (flip R).
 Proof. firstorder. Qed.
-  
-Program Instance compose_morphism A B C R鈧� R鈧� R鈧� :
-  Morphism ((R鈧� ==> R鈧�) ==> (R鈧� ==> R鈧�) ==> (R鈧� ==> R鈧�)) (@compose A B C).
+
+Program Instance compose_proper A B C R鈧� R鈧� R鈧� :
+  Proper ((R鈧� ==> R鈧�) ==> (R鈧� ==> R鈧�) ==> (R鈧� ==> R鈧�)) (@compose A B C).
 
   Next Obligation.
   Proof.
@@ -280,7 +300,7 @@ Program Instance compose_morphism A B C R鈧� R鈧� R鈧� :
     unfold compose. apply H. apply H0. apply H1.
   Qed.
 
-(** Coq functions are morphisms for leibniz equality, 
+(** Coq functions are morphisms for Leibniz equality,
    applied only if really needed. *)
 
 Instance reflexive_eq_dom_reflexive (A : Type) `(Reflexive B R') :
@@ -289,13 +309,13 @@ Proof. simpl_relation. Qed.
 
 (** [respectful] is a morphism for relation equivalence. *)
 
-Instance respectful_morphism : 
-  Morphism (relation_equivalence ++> relation_equivalence ++> relation_equivalence) (@respectful A B).
+Instance respectful_morphism :
+  Proper (relation_equivalence ++> relation_equivalence ++> relation_equivalence) (@respectful A B).
 Proof.
   reduce.
   unfold respectful, relation_equivalence, predicate_equivalence in * ; simpl in *.
   split ; intros.
-  
+
     rewrite <- H0.
     apply H1.
     rewrite H.
@@ -309,43 +329,50 @@ Qed.
 
 (** Every element in the carrier of a reflexive relation is a morphism for this relation.
    We use a proxy class for this case which is used internally to discharge reflexivity constraints.
-   The [Reflexive] instance will almost always be used, but it won't apply in general to any kind of 
-   [Morphism (A -> B) _ _] goal, making proof-search much slower. A cleaner solution would be to be able
+   The [Reflexive] instance will almost always be used, but it won't apply in general to any kind of
+   [Proper (A -> B) _ _] goal, making proof-search much slower. A cleaner solution would be to be able
    to set different priorities in different hint bases and select a particular hint database for
-   resolution of a type class constraint.*) 
+   resolution of a type class constraint.*)
 
-Class MorphismProxy {A} (R : relation A) (m : A) : Prop :=
-  respect_proxy : R m m.
+Class ProperProxy {A} (R : relation A) (m : A) : Prop :=
+  proper_proxy : R m m.
 
-Instance reflexive_morphism_proxy
-  `(Reflexive A R) (x : A) : MorphismProxy R x | 1.
+Lemma eq_proper_proxy A (x : A) : ProperProxy (@eq A) x.
 Proof. firstorder. Qed.
 
-Instance morphism_morphism_proxy
-  `(Morphism A R x) : MorphismProxy R x | 2.
+Lemma reflexive_proper_proxy `(Reflexive A R) (x : A) : ProperProxy R x.
 Proof. firstorder. Qed.
 
+Lemma proper_proper_proxy `(Proper A R x) : ProperProxy R x.
+Proof. firstorder. Qed.
+
+Hint Extern 1 (ProperProxy _ _) => 
+  class_apply @eq_proper_proxy || class_apply @reflexive_proper_proxy : typeclass_instances.
+Hint Extern 2 (ProperProxy ?R _) => not_evar R; class_apply @proper_proper_proxy : typeclass_instances.
+
 (** [R] is Reflexive, hence we can build the needed proof. *)
 
-Lemma Reflexive_partial_app_morphism `(Morphism (A -> B) (R ==> R') m, MorphismProxy A R x) :
-   Morphism R' (m x).
+Lemma Reflexive_partial_app_morphism `(Proper (A -> B) (R ==> R') m, ProperProxy A R x) :
+   Proper R' (m x).
 Proof. simpl_relation. Qed.
 
 Class Params {A : Type} (of : A) (arity : nat).
 
 Class PartialApplication.
 
-Ltac partial_application_tactic := 
+CoInductive normalization_done : Prop := did_normalization.
+
+Ltac partial_application_tactic :=
   let rec do_partial_apps H m :=
     match m with
-      | ?m' ?x => eapply @Reflexive_partial_app_morphism ; [do_partial_apps H m'|clear H]
+      | ?m' ?x => class_apply @Reflexive_partial_app_morphism ; [do_partial_apps H m'|clear H]
       | _ => idtac
     end
   in
   let rec do_partial H ar m :=
     match ar with
       | 0 => do_partial_apps H m
-      | S ?n' => 
+      | S ?n' =>
         match m with
           ?m' ?x => do_partial H n' m'
         end
@@ -357,25 +384,24 @@ Ltac partial_application_tactic :=
     let v := eval compute in n in clear n ;
     let H := fresh in
       assert(H:Params m' v) by typeclasses eauto ;
-      let v' := eval compute in v in 
+      let v' := eval compute in v in subst m';
       do_partial H v' m
  in
   match goal with
-    | [ _ : subrelation_done |- _ ] => fail 1
     | [ _ : normalization_done |- _ ] => fail 1
     | [ _ : @Params _ _ _ |- _ ] => fail 1
-    | [ |- @Morphism ?T _ (?m ?x) ] => 
-      match goal with 
-        | [ _ : PartialApplication |- _ ] => 
-          eapply @Reflexive_partial_app_morphism
-        | _ => 
-          on_morphism (m x) || 
-            (eapply @Reflexive_partial_app_morphism ;
+    | [ |- @Proper ?T _ (?m ?x) ] =>
+      match goal with
+        | [ _ : PartialApplication |- _ ] =>
+          class_apply @Reflexive_partial_app_morphism
+        | _ =>
+          on_morphism (m x) ||
+            (class_apply @Reflexive_partial_app_morphism ;
               [ pose Build_PartialApplication | idtac ])
       end
   end.
 
-Hint Extern 4 (@Morphism _ _ _) => partial_application_tactic : typeclass_instances.
+Hint Extern 4 (@Proper _ _ _) => partial_application_tactic : typeclass_instances.
 
 Lemma inverse_respectful : forall (A : Type) (R : relation A) (B : Type) (R' : relation B),
   relation_equivalence (inverse (R ==> R')) (inverse R ==> inverse R').
@@ -387,7 +413,7 @@ Qed.
 
 (** Special-purpose class to do normalization of signatures w.r.t. inverse. *)
 
-Class Normalizes (A : Type) (m : relation A) (m' : relation A) : Prop := 
+Class Normalizes (A : Type) (m : relation A) (m' : relation A) : Prop :=
   normalizes : relation_equivalence m m'.
 
 (** Current strategy: add [inverse] everywhere and reduce using [subrelation]
@@ -400,19 +426,19 @@ Qed.
 
 Lemma inverse_arrow `(NA : Normalizes A R (inverse R'''), NB : Normalizes B R' (inverse R'')) :
   Normalizes (A -> B) (R ==> R') (inverse (R''' ==> R'')%signature).
-Proof. unfold Normalizes. intros.
+Proof. unfold Normalizes in *. intros.
   rewrite NA, NB. firstorder.
 Qed.
 
-Ltac inverse :=   
+Ltac inverse :=
   match goal with
-    | [ |- Normalizes _ (respectful _ _) _ ] => eapply @inverse_arrow
-    | _ => eapply @inverse_atom
+    | [ |- Normalizes _ (respectful _ _) _ ] => class_apply @inverse_arrow
+    | _ => class_apply @inverse_atom
   end.
 
 Hint Extern 1 (Normalizes _ _ _) => inverse : typeclass_instances.
 
-(** Treating inverse: can't make them direct instances as we 
+(** Treating inverse: can't make them direct instances as we
    need at least a [flip] present in the goal. *)
 
 Lemma inverse1 `(subrelation A R' R) : subrelation (inverse (inverse R')) R.
@@ -421,18 +447,25 @@ Proof. firstorder. Qed.
 Lemma inverse2 `(subrelation A R R') : subrelation R (inverse (inverse R')).
 Proof. firstorder. Qed.
 
-Hint Extern 1 (subrelation (flip _) _) => eapply @inverse1 : typeclass_instances.
-Hint Extern 1 (subrelation _ (flip _)) => eapply @inverse2 : typeclass_instances.
+Hint Extern 1 (subrelation (flip _) _) => class_apply @inverse1 : typeclass_instances.
+Hint Extern 1 (subrelation _ (flip _)) => class_apply @inverse2 : typeclass_instances.
+
+(** That's if and only if *)
+
+Lemma eq_subrelation `(Reflexive A R) : subrelation (@eq A) R.
+Proof. simpl_relation. Qed.
+
+(* Hint Extern 3 (subrelation eq ?R) => not_evar R ; class_apply eq_subrelation : typeclass_instances. *)
 
 (** Once we have normalized, we will apply this instance to simplify the problem. *)
 
-Definition morphism_inverse_morphism `(mor : Morphism A R m) : Morphism (inverse R) m := mor.
+Definition proper_inverse_proper `(mor : Proper A R m) : Proper (inverse R) m := mor.
 
-Hint Extern 2 (@Morphism _ (flip _) _) => eapply @morphism_inverse_morphism : typeclass_instances.
+Hint Extern 2 (@Proper _ (flip _) _) => class_apply @proper_inverse_proper : typeclass_instances.
 
 (** Bootstrap !!! *)
 
-Instance morphism_morphism : Morphism (relation_equivalence ==> @eq _ ==> iff) (@Morphism A).
+Instance proper_proper : Proper (relation_equivalence ==> eq ==> iff) (@Proper A).
 Proof.
   simpl_relation.
   reduce in H.
@@ -443,37 +476,139 @@ Proof.
   apply H0.
 Qed.
 
-Lemma morphism_releq_morphism `(Normalizes A R R', Morphism _ R' m) : Morphism R m.
+Lemma proper_normalizes_proper `(Normalizes A R0 R1, Proper A R1 m) : Proper R0 m.
 Proof.
-  intros.
-
-  pose respect as r.
-  pose normalizes as norm.
-  setoid_rewrite norm.
+  red in H, H0.
+  setoid_rewrite H.
   assumption.
 Qed.
 
-Ltac morphism_normalization := 
+Ltac proper_normalization :=
   match goal with
-    | [ _ : subrelation_done |- _ ] => fail 1
     | [ _ : normalization_done |- _ ] => fail 1
-    | [ |- @Morphism _ _ _ ] => let H := fresh "H" in
-      set(H:=did_normalization) ; eapply @morphism_releq_morphism
+    | [ _ : apply_subrelation |- @Proper _ ?R _ ] => let H := fresh "H" in
+      set(H:=did_normalization) ; class_apply @proper_normalizes_proper
   end.
 
-Hint Extern 6 (@Morphism _ _ _) => morphism_normalization : typeclass_instances.
+Hint Extern 6 (@Proper _ _ _) => proper_normalization : typeclass_instances.
 
 (** Every reflexive relation gives rise to a morphism, only for immediately solving goals without variables. *)
 
-Lemma reflexive_morphism `{Reflexive A R} (x : A)
-   : Morphism R x.
+Lemma reflexive_proper `{Reflexive A R} (x : A)
+   : Proper R x.
 Proof. firstorder. Qed.
 
-Ltac morphism_reflexive :=
+Lemma proper_eq A (x : A) : Proper (@eq A) x.
+Proof. intros. apply reflexive_proper. Qed.
+
+Ltac proper_reflexive :=
   match goal with
     | [ _ : normalization_done |- _ ] => fail 1
-    | [ _ : subrelation_done |- _ ] => fail 1
-    | [ |- @Morphism _ _ _ ] => eapply @reflexive_morphism
+    | _ => class_apply proper_eq || class_apply @reflexive_proper
   end.
 
-Hint Extern 7 (@Morphism _ _ _) => morphism_reflexive : typeclass_instances.
+Hint Extern 7 (@Proper _ _ _) => proper_reflexive : typeclass_instances.
+
+
+(** When the relation on the domain is symmetric, we can
+    inverse the relation on the codomain. Same for binary functions. *)
+
+Lemma proper_sym_flip :
+ forall `(Symmetric A R1)`(Proper (A->B) (R1==>R2) f),
+ Proper (R1==>inverse R2) f.
+Proof.
+intros A R1 Sym B R2 f Hf.
+intros x x' Hxx'. apply Hf, Sym, Hxx'.
+Qed.
+
+Lemma proper_sym_flip_2 :
+ forall `(Symmetric A R1)`(Symmetric B R2)`(Proper (A->B->C) (R1==>R2==>R3) f),
+ Proper (R1==>R2==>inverse R3) f.
+Proof.
+intros A R1 Sym1 B R2 Sym2 C R3 f Hf.
+intros x x' Hxx' y y' Hyy'. apply Hf; auto.
+Qed.
+
+(** When the relation on the domain is symmetric, a predicate is
+  compatible with [iff] as soon as it is compatible with [impl].
+  Same with a binary relation. *)
+
+Lemma proper_sym_impl_iff : forall `(Symmetric A R)`(Proper _ (R==>impl) f),
+ Proper (R==>iff) f.
+Proof.
+intros A R Sym f Hf x x' Hxx'. repeat red in Hf. split; eauto.
+Qed.
+
+Lemma proper_sym_impl_iff_2 :
+ forall `(Symmetric A R)`(Symmetric B R')`(Proper _ (R==>R'==>impl) f),
+ Proper (R==>R'==>iff) f.
+Proof.
+intros A R Sym B R' Sym' f Hf x x' Hxx' y y' Hyy'.
+repeat red in Hf. split; eauto.
+Qed.
+
+(** A [PartialOrder] is compatible with its underlying equivalence. *)
+
+Instance PartialOrder_proper `(PartialOrder A eqA R) :
+  Proper (eqA==>eqA==>iff) R.
+Proof.
+intros.
+apply proper_sym_impl_iff_2; auto with *.
+intros x x' Hx y y' Hy Hr.
+transitivity x.
+generalize (partial_order_equivalence x x'); compute; intuition.
+transitivity y; auto.
+generalize (partial_order_equivalence y y'); compute; intuition.
+Qed.
+
+(** From a [PartialOrder] to the corresponding [StrictOrder]:
+     [lt = le /\ ~eq].
+    If the order is total, we could also say [gt = ~le]. *)
+
+Lemma PartialOrder_StrictOrder `(PartialOrder A eqA R) :
+  StrictOrder (relation_conjunction R (complement eqA)).
+Proof.
+split; compute.
+intros x (_,Hx). apply Hx, Equivalence_Reflexive.
+intros x y z (Hxy,Hxy') (Hyz,Hyz'). split.
+apply PreOrder_Transitive with y; assumption.
+intro Hxz.
+apply Hxy'.
+apply partial_order_antisym; auto.
+rewrite Hxz; auto.
+Qed.
+
+Hint Extern 4 (StrictOrder (relation_conjunction _ _)) => 
+  class_apply PartialOrder_StrictOrder : typeclass_instances.
+
+(** From a [StrictOrder] to the corresponding [PartialOrder]:
+     [le = lt \/ eq].
+    If the order is total, we could also say [ge = ~lt]. *)
+
+Lemma StrictOrder_PreOrder
+ `(Equivalence A eqA, StrictOrder A R, Proper _ (eqA==>eqA==>iff) R) :
+ PreOrder (relation_disjunction R eqA).
+Proof.
+split.
+intros x. right. reflexivity.
+intros x y z [Hxy|Hxy] [Hyz|Hyz].
+left. transitivity y; auto.
+left. rewrite <- Hyz; auto.
+left. rewrite Hxy; auto.
+right. transitivity y; auto.
+Qed.
+
+Hint Extern 4 (PreOrder (relation_disjunction _ _)) => 
+  class_apply StrictOrder_PreOrder : typeclass_instances.
+
+Lemma StrictOrder_PartialOrder
+  `(Equivalence A eqA, StrictOrder A R, Proper _ (eqA==>eqA==>iff) R) :
+  PartialOrder eqA (relation_disjunction R eqA).
+Proof.
+intros. intros x y. compute. intuition.
+elim (StrictOrder_Irreflexive x).
+transitivity y; auto.
+Qed.
+
+Hint Extern 4 (PartialOrder _ (relation_disjunction _ _)) => 
+  class_apply StrictOrder_PartialOrder : typeclass_instances.
diff --git a/theories/Classes/Morphisms_Prop.v b/theories/Classes/Morphisms_Prop.v
index 3bbd56cf..2dc033d2 100644
--- a/theories/Classes/Morphisms_Prop.v
+++ b/theories/Classes/Morphisms_Prop.v
@@ -6,81 +6,83 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* Morphism instances for propositional connectives.
- 
+(** * [Proper] instances for propositional connectives.
+
    Author: Matthieu Sozeau
-   Institution: LRI, CNRS UMR 8623 - Universit脙copyright Paris Sud
-   91405 Orsay, France *)
+   Institution: LRI, CNRS UMR 8623 - University Paris Sud
+*)
 
 Require Import Coq.Classes.Morphisms.
 Require Import Coq.Program.Basics.
 Require Import Coq.Program.Tactics.
 
+Local Obligation Tactic := simpl_relation.
+
 (** Standard instances for [not], [iff] and [impl]. *)
 
 (** Logical negation. *)
 
 Program Instance not_impl_morphism :
-  Morphism (impl --> impl) not.
+  Proper (impl --> impl) not | 1.
 
-Program Instance not_iff_morphism : 
-  Morphism (iff ++> iff) not.
+Program Instance not_iff_morphism :
+  Proper (iff ++> iff) not.
 
 (** Logical conjunction. *)
 
 Program Instance and_impl_morphism :
-  Morphism (impl ==> impl ==> impl) and.
+  Proper (impl ==> impl ==> impl) and | 1.
 
-Program Instance and_iff_morphism : 
-  Morphism (iff ==> iff ==> iff) and.
+Program Instance and_iff_morphism :
+  Proper (iff ==> iff ==> iff) and.
 
 (** Logical disjunction. *)
 
-Program Instance or_impl_morphism : 
-  Morphism (impl ==> impl ==> impl) or.
+Program Instance or_impl_morphism :
+  Proper (impl ==> impl ==> impl) or | 1.
 
-Program Instance or_iff_morphism : 
-  Morphism (iff ==> iff ==> iff) or.
+Program Instance or_iff_morphism :
+  Proper (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.
+Program Instance iff_iff_iff_impl_morphism : Proper (iff ==> iff ==> iff) impl.
 
 (** Morphisms for quantifiers *)
 
-Program Instance ex_iff_morphism {A : Type} : Morphism (pointwise_relation A iff ==> iff) (@ex A).
+Program Instance ex_iff_morphism {A : Type} : Proper (pointwise_relation A iff ==> iff) (@ex A).
 
   Next Obligation.
   Proof.
-    unfold pointwise_relation in H.     
+    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.
+    destruct H0 as [x1 H1].
+    exists x1. rewrite H in H1. assumption.
+
+    destruct H0 as [x1 H1].
+    exists x1. rewrite H. assumption.
   Qed.
 
 Program Instance ex_impl_morphism {A : Type} :
-  Morphism (pointwise_relation A impl ==> impl) (@ex A).
+  Proper (pointwise_relation A impl ==> impl) (@ex A) | 1.
 
   Next Obligation.
   Proof.
-    unfold pointwise_relation in H.  
+    unfold pointwise_relation in H.
     exists H0. apply H. assumption.
   Qed.
 
-Program Instance ex_inverse_impl_morphism {A : Type} : 
-  Morphism (pointwise_relation A (inverse impl) ==> inverse impl) (@ex A).
+Program Instance ex_inverse_impl_morphism {A : Type} :
+  Proper (pointwise_relation A (inverse impl) ==> inverse impl) (@ex A) | 1.
 
   Next Obligation.
   Proof.
-    unfold pointwise_relation in H.  
+    unfold pointwise_relation in H.
     exists H0. apply H. assumption.
   Qed.
 
-Program Instance all_iff_morphism {A : Type} : 
-  Morphism (pointwise_relation A iff ==> iff) (@all A).
+Program Instance all_iff_morphism {A : Type} :
+  Proper (pointwise_relation A iff ==> iff) (@all A).
 
   Next Obligation.
   Proof.
@@ -88,18 +90,18 @@ Program Instance all_iff_morphism {A : Type} :
     intuition ; specialize (H x0) ; intuition.
   Qed.
 
-Program Instance all_impl_morphism {A : Type} : 
-  Morphism (pointwise_relation A impl ==> impl) (@all A).
-  
+Program Instance all_impl_morphism {A : Type} :
+  Proper (pointwise_relation A impl ==> impl) (@all A) | 1.
+
   Next Obligation.
   Proof.
     unfold pointwise_relation, all in *.
     intuition ; specialize (H x0) ; intuition.
   Qed.
 
-Program Instance all_inverse_impl_morphism {A : Type} : 
-  Morphism (pointwise_relation A (inverse impl) ==> inverse impl) (@all A).
-  
+Program Instance all_inverse_impl_morphism {A : Type} :
+  Proper (pointwise_relation A (inverse impl) ==> inverse impl) (@all A) | 1.
+
   Next Obligation.
   Proof.
     unfold pointwise_relation, all in *.
diff --git a/theories/Classes/Morphisms_Relations.v b/theories/Classes/Morphisms_Relations.v
index 4654e654..d8365abc 100644
--- a/theories/Classes/Morphisms_Relations.v
+++ b/theories/Classes/Morphisms_Relations.v
@@ -6,23 +6,25 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* Morphism instances for relations.
- 
+(** * Morphism instances for relations.
+
    Author: Matthieu Sozeau
-   Institution: LRI, CNRS UMR 8623 - Universit脙copyright Paris Sud
-   91405 Orsay, France *)
+   Institution: LRI, CNRS UMR 8623 - University Paris Sud
+*)
 
 Require Import Relation_Definitions.
 Require Import Coq.Classes.Morphisms.
 Require Import Coq.Program.Program.
 
+Generalizable Variables A l.
+
 (** Morphisms for relations *)
 
-Instance relation_conjunction_morphism : Morphism (relation_equivalence (A:=A) ==>
+Instance relation_conjunction_morphism : Proper (relation_equivalence (A:=A) ==>
   relation_equivalence ==> relation_equivalence) relation_conjunction.
   Proof. firstorder. Qed.
 
-Instance relation_disjunction_morphism : Morphism (relation_equivalence (A:=A) ==>
+Instance relation_disjunction_morphism : Proper (relation_equivalence (A:=A) ==>
   relation_equivalence ==> relation_equivalence) relation_disjunction.
   Proof. firstorder. Qed.
 
@@ -31,25 +33,25 @@ Instance relation_disjunction_morphism : Morphism (relation_equivalence (A:=A) =
 Require Import List.
 
 Lemma predicate_equivalence_pointwise (l : list Type) :
-  Morphism (@predicate_equivalence l ==> pointwise_lifting iff l) id.
+  Proper (@predicate_equivalence l ==> pointwise_lifting iff l) id.
 Proof. do 2 red. unfold predicate_equivalence. auto. Qed.
 
 Lemma predicate_implication_pointwise (l : list Type) :
-  Morphism (@predicate_implication l ==> pointwise_lifting impl l) id.
+  Proper (@predicate_implication l ==> pointwise_lifting impl l) 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]. *)
+(** 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 (pointwise_relation A iff)) id.
+  Proper (relation_equivalence ==> pointwise_relation A (pointwise_relation A iff)) id.
 Proof. intro. apply (predicate_equivalence_pointwise (cons A (cons A nil))). Qed.
 
 Instance subrelation_pointwise :
-  Morphism (subrelation ==> pointwise_relation A (pointwise_relation A impl)) id.
+  Proper (subrelation ==> pointwise_relation A (pointwise_relation A impl)) id.
 Proof. intro. apply (predicate_implication_pointwise (cons A (cons A nil))). Qed.
 
 
-Lemma inverse_pointwise_relation A (R : relation A) : 
+Lemma inverse_pointwise_relation A (R : relation A) :
   relation_equivalence (pointwise_relation A (inverse R)) (inverse (pointwise_relation A R)).
 Proof. intros. split; firstorder. Qed.
diff --git a/theories/Classes/RelationClasses.v b/theories/Classes/RelationClasses.v
index e1de9ee9..9b848551 100644
--- a/theories/Classes/RelationClasses.v
+++ b/theories/Classes/RelationClasses.v
@@ -1,3 +1,4 @@
+(* -*- coding: utf-8 -*- *)
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
 (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
@@ -6,14 +7,15 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* Typeclass-based relations, tactics and standard instances.
+(** *  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
-   91405 Orsay, France *)
+   Institution: LRI, CNRS UMR 8623 - University Paris Sud
+*)
 
-(* $Id: RelationClasses.v 12187 2009-06-13 19:36:59Z msozeau $ *)
+(* $Id$ *)
 
 Require Export Coq.Classes.Init.
 Require Import Coq.Program.Basics.
@@ -42,16 +44,18 @@ Unset Strict Implicit.
 Class Reflexive {A} (R : relation A) :=
   reflexivity : forall x, R x x.
 
-Class Irreflexive {A} (R : relation A) := 
-  irreflexivity :> Reflexive (complement R).
+Class Irreflexive {A} (R : relation A) :=
+  irreflexivity : Reflexive (complement R).
 
-Class Symmetric {A} (R : relation A) := 
+Hint Extern 1 (Reflexive (complement _)) => class_apply @irreflexivity : typeclass_instances.
+
+Class Symmetric {A} (R : relation A) :=
   symmetry : forall x y, R x y -> R y x.
 
-Class Asymmetric {A} (R : relation A) := 
+Class Asymmetric {A} (R : relation A) :=
   asymmetry : forall x y, R x y -> R y x -> False.
 
-Class Transitive {A} (R : relation A) := 
+Class Transitive {A} (R : relation A) :=
   transitivity : forall x y z, R x y -> R y z -> R x z.
 
 Hint Resolve @irreflexivity : ord.
@@ -61,7 +65,7 @@ Unset Implicit Arguments.
 (** A HintDb for relations. *)
 
 Ltac solve_relation :=
-  match goal with 
+  match goal with
   | [ |- ?R ?x ?x ] => reflexivity
   | [ H : ?R ?x ?y |- ?R ?y ?x ] => symmetry ; exact H
   end.
@@ -70,34 +74,39 @@ Hint Extern 4 => solve_relation : relations.
 
 (** We can already dualize all these properties. *)
 
-Program Instance flip_Reflexive `(Reflexive A R) : Reflexive (flip R) :=
-  reflexivity (R:=R).
+Generalizable Variables A B C D R S T U l eqA eqB eqC eqD.
 
-Program Instance flip_Irreflexive `(Irreflexive A R) : Irreflexive (flip R) :=
-  irreflexivity (R:=R).
+Program Lemma flip_Reflexive `(Reflexive A R) : Reflexive (flip R).
+Proof. tauto. Qed.
+
+Hint Extern 3 (Reflexive (flip _)) => apply flip_Reflexive : typeclass_instances.
 
-Program Instance flip_Symmetric `(Symmetric A R) : Symmetric (flip R).
+Program Definition flip_Irreflexive `(Irreflexive A R) : Irreflexive (flip R) :=
+  irreflexivity (R:=R).
 
-  Solve Obligations using unfold flip ; intros ; tcapp symmetry ; assumption.
+Program Definition flip_Symmetric `(Symmetric A R) : Symmetric (flip R) :=
+  fun x y H => symmetry (R:=R) H.
 
-Program Instance flip_Asymmetric `(Asymmetric A R) : Asymmetric (flip R).
-  
-  Solve Obligations using program_simpl ; unfold flip in * ; intros ; typeclass_app asymmetry ; eauto.
+Program Definition flip_Asymmetric `(Asymmetric A R) : Asymmetric (flip R) :=
+  fun x y H H' => asymmetry (R:=R) H H'.
 
-Program Instance flip_Transitive `(Transitive A R) : Transitive (flip R).
+Program Definition flip_Transitive `(Transitive A R) : Transitive (flip R) :=
+  fun x y z H H' => transitivity (R:=R) H' H.
 
-  Solve Obligations using unfold flip ; program_simpl ; typeclass_app transitivity ; eauto.
+Hint Extern 3 (Irreflexive (flip _)) => class_apply flip_Irreflexive : typeclass_instances.
+Hint Extern 3 (Symmetric (flip _)) => class_apply flip_Symmetric : typeclass_instances.
+Hint Extern 3 (Asymmetric (flip _)) => class_apply flip_Asymmetric : typeclass_instances.
+Hint Extern 3 (Transitive (flip _)) => class_apply flip_Transitive : typeclass_instances.
 
-Program Instance Reflexive_complement_Irreflexive `(Reflexive A (R : relation A))
+Definition Reflexive_complement_Irreflexive `(Reflexive A (R : relation A))
    : Irreflexive (complement R).
+Proof. firstorder. Qed.
 
-  Next Obligation. 
-  Proof. firstorder. Qed.
-
-Program Instance complement_Symmetric `(Symmetric A (R : relation A)) : Symmetric (complement R).
+Definition complement_Symmetric `(Symmetric A (R : relation A)) : Symmetric (complement R).
+Proof. firstorder. Qed.
 
-  Next Obligation.
-  Proof. firstorder. Qed.
+Hint Extern 3 (Symmetric (complement _)) => class_apply complement_Symmetric : typeclass_instances.
+Hint Extern 3 (Irreflexive (complement _)) => class_apply Reflexive_complement_Irreflexive : typeclass_instances.
 
 (** * Standard instances. *)
 
@@ -117,7 +126,7 @@ Tactic Notation "reduce" "in" hyp(Hid) := reduce_hyp Hid.
 
 Ltac reduce := reduce_goal.
 
-Tactic Notation "apply" "*" constr(t) := 
+Tactic Notation "apply" "*" constr(t) :=
   first [ refine t | refine (t _) | refine (t _ _) | refine (t _ _ _) | refine (t _ _ _ _) |
     refine (t _ _ _ _ _) | refine (t _ _ _ _ _ _) | refine (t _ _ _ _ _ _ _) ].
 
@@ -125,7 +134,7 @@ Ltac simpl_relation :=
   unfold flip, impl, arrow ; try reduce ; program_simpl ;
     try ( solve [ intuition ]).
 
-Ltac obligation_tactic ::= simpl_relation.
+Local Obligation Tactic := simpl_relation.
 
 (** Logical implication. *)
 
@@ -174,13 +183,14 @@ Instance Equivalence_PER `(Equivalence A R) : PER R | 10 :=
 (** We can now define antisymmetry w.r.t. an equivalence relation on the carrier. *)
 
 Class Antisymmetric A eqA `{equ : Equivalence A eqA} (R : relation A) :=
-  antisymmetry : forall x y, R x y -> R y x -> eqA x y.
+  antisymmetry : forall {x y}, R x y -> R y x -> eqA x y.
 
-Program Instance flip_antiSymmetric `(Antisymmetric A eqA R) :
-  ! Antisymmetric A eqA (flip R).
+Program Definition flip_antiSymmetric `(Antisymmetric A eqA R) :
+  Antisymmetric A eqA (flip R).
+Proof. firstorder. Qed.
 
 (** Leibinz equality [eq] is an equivalence relation.
-   The instance has low priority as it is always applicable 
+   The instance has low priority as it is always applicable
    if only the type is constrained. *)
 
 Program Instance eq_equivalence : Equivalence (@eq A) | 10.
@@ -193,26 +203,24 @@ Program Instance iff_equivalence : Equivalence iff.
    The resulting theory can be applied to homogeneous binary relations but also to
    arbitrary n-ary predicates. *)
 
-Require Import Coq.Lists.List.
+Local Open Scope list_scope.
 
 (* Notation " [ ] " := nil : list_scope. *)
 (* Notation " [ x ; .. ; y ] " := (cons x .. (cons y nil) ..) (at level 1) : list_scope. *)
 
-(* Open Local Scope list_scope. *)
-
 (** A compact representation of non-dependent arities, with the codomain singled-out. *)
 
-Fixpoint arrows (l : list Type) (r : Type) : Type := 
-  match l with 
+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 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 unary_operation A := arrows (A::nil) A.
+Definition binary_operation A := arrows (A::A::nil) A.
+Definition ternary_operation A := arrows (A::A::A::nil) A.
 
 (** We define n-ary [predicate]s as functions into [Prop]. *)
 
@@ -220,13 +228,13 @@ Notation predicate l := (arrows l Prop).
 
 (** Unary predicates, or sets. *)
 
-Definition unary_predicate A := predicate (cons A nil).
+Definition unary_predicate A := predicate (A::nil).
 
 (** Homogeneous binary relations, equivalent to [relation A]. *)
 
-Definition binary_relation A := predicate (cons A (cons A nil)).
+Definition binary_relation A := predicate (A::A::nil).
 
-(** We can close a predicate by universal or existential quantification. *) 
+(** We can close a predicate by universal or existential quantification. *)
 
 Fixpoint predicate_all (l : list Type) : predicate l -> Prop :=
   match l with
@@ -240,7 +248,7 @@ Fixpoint predicate_exists (l : list Type) : predicate l -> Prop :=
     | 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 
+(** Pointwise extension of a binary operation on [T] to a binary operation
    on functions whose codomain is [T].
    For an operator on [Prop] this lifts the operator to a binary operation. *)
 
@@ -248,7 +256,7 @@ Fixpoint pointwise_extension {T : Type} (op : binary_operation T)
   (l : list Type) : binary_operation (arrows l T) :=
   match l with
     | nil => fun R R' => op R R'
-    | A :: tl => fun R R' => 
+    | A :: tl => fun R R' =>
       fun x => pointwise_extension op tl (R x) (R' x)
   end.
 
@@ -257,7 +265,7 @@ Fixpoint pointwise_extension {T : Type} (op : binary_operation T)
 Fixpoint pointwise_lifting (op : binary_relation Prop)  (l : list Type) : binary_relation (predicate l) :=
   match l with
     | nil => fun R R' => op R R'
-    | A :: tl => fun R R' => 
+    | A :: tl => fun R R' =>
       forall x, pointwise_lifting op tl (R x) (R' x)
   end.
 
@@ -289,7 +297,7 @@ Infix "\鈭�/" := predicate_union (at level 85, right associativity) : predicate_
 
 (** The always [True] and always [False] predicates. *)
 
-Fixpoint true_predicate {l : list Type} : predicate l := 
+Fixpoint true_predicate {l : list Type} : predicate l :=
   match l with
     | nil => True
     | A :: tl => fun _ => @true_predicate tl
@@ -306,17 +314,13 @@ Notation "鈭欌姤鈭�" := false_predicate : predicate_scope.
 
 (** Predicate equivalence is an equivalence, and predicate implication defines a preorder. *)
 
-Program Instance predicate_equivalence_equivalence :
-  Equivalence (@predicate_equivalence l).
-
+Program Instance predicate_equivalence_equivalence : Equivalence (@predicate_equivalence l).
   Next Obligation.
     induction l ; firstorder.
   Qed.
-
   Next Obligation.
     induction l ; firstorder.
   Qed.
-  
   Next Obligation.
     fold pointwise_lifting.
     induction l. firstorder.
@@ -326,59 +330,59 @@ Program Instance predicate_equivalence_equivalence :
 
 Program Instance predicate_implication_preorder :
   PreOrder (@predicate_implication l).
-
   Next Obligation.
     induction l ; firstorder.
   Qed.
-
   Next Obligation.
     induction l. firstorder.
-    unfold predicate_implication in *. simpl in *. 
+    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, 
+(** 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)).
+  @predicate_equivalence (_::_::nil).
 
 Class subrelation {A:Type} (R R' : relation A) : Prop :=
-  is_subrelation : @predicate_implication (cons A (cons A nil)) R R'.
+  is_subrelation : @predicate_implication (A::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'.
+  @predicate_intersection (A::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'.
+  @predicate_union (A::A::nil) R R'.
 
 (** Relation equivalence is an equivalence, and subrelation defines a partial order. *)
 
+Set Automatic Introduction.
+
 Instance relation_equivalence_equivalence (A : Type) :
   Equivalence (@relation_equivalence A).
-Proof. intro A. exact (@predicate_equivalence_equivalence (cons A (cons A nil))). Qed.
+Proof. exact (@predicate_equivalence_equivalence (A::A::nil)). Qed.
 
-Instance relation_implication_preorder : PreOrder (@subrelation A).
-Proof. intro A. exact (@predicate_implication_preorder (cons A (cons A nil))). Qed.
+Instance relation_implication_preorder A : PreOrder (@subrelation A).
+Proof. exact (@predicate_implication_preorder (A::A::nil)). Qed.
 
 (** *** Partial Order.
    A partial order is a preorder which is additionally antisymmetric.
-   We give an equivalent definition, up-to an equivalence relation 
+   We give an equivalent definition, up-to an equivalence relation
    on the carrier. *)
 
 Class PartialOrder {A} eqA `{equ : Equivalence A eqA} R `{preo : PreOrder A 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 
+(** The equivalence proof is sufficient for proving that [R] must be a morphism
    for equivalence (see Morphisms).
    It is also sufficient to show that [R] is antisymmetric w.r.t. [eqA] *)
 
 Instance partial_order_antisym `(PartialOrder A eqA R) : ! Antisymmetric A eqA R.
 Proof with auto.
-  reduce_goal. 
-  pose proof partial_order_equivalence as poe. do 3 red in poe. 
+  reduce_goal.
+  pose proof partial_order_equivalence as poe. do 3 red in poe.
   apply <- poe. firstorder.
 Qed.
 
@@ -392,5 +396,52 @@ Program Instance subrelation_partial_order :
     unfold relation_equivalence in *. firstorder.
   Qed.
 
-Typeclasses Opaque arrows predicate_implication predicate_equivalence 
+Typeclasses Opaque arrows predicate_implication predicate_equivalence
   relation_equivalence pointwise_lifting.
+
+(** Rewrite relation on a given support: declares a relation as a rewrite
+   relation for use by the generalized rewriting tactic.
+   It helps choosing if a rewrite should be handled
+   by the generalized or the regular rewriting tactic using leibniz equality.
+   Users can declare an [RewriteRelation A RA] anywhere to declare default
+   relations. This is also done automatically by the [Declare Relation A RA]
+   commands. *)
+
+Class RewriteRelation {A : Type} (RA : relation A).
+
+Instance: RewriteRelation impl.
+Instance: RewriteRelation iff.
+Instance: RewriteRelation (@relation_equivalence A).
+
+(** Any [Equivalence] declared in the context is automatically considered
+   a rewrite relation. *)
+
+Instance equivalence_rewrite_relation `(Equivalence A eqA) : RewriteRelation eqA.
+
+(** Strict Order *)
+
+Class StrictOrder {A : Type} (R : relation A) := {
+  StrictOrder_Irreflexive :> Irreflexive R ;
+  StrictOrder_Transitive :> Transitive R
+}.
+
+Instance StrictOrder_Asymmetric `(StrictOrder A R) : Asymmetric R.
+Proof. firstorder. Qed.
+
+(** Inversing a [StrictOrder] gives another [StrictOrder] *)
+
+Lemma StrictOrder_inverse `(StrictOrder A R) : StrictOrder (inverse R).
+Proof. firstorder. Qed.
+
+(** Same for [PartialOrder]. *)
+
+Lemma PreOrder_inverse `(PreOrder A R) : PreOrder (inverse R).
+Proof. firstorder. Qed.
+
+Hint Extern 3 (StrictOrder (inverse _)) => class_apply StrictOrder_inverse : typeclass_instances.
+Hint Extern 3 (PreOrder (inverse _)) => class_apply PreOrder_inverse : typeclass_instances.
+
+Lemma PartialOrder_inverse `(PartialOrder A eqA R) : PartialOrder eqA (inverse R).
+Proof. firstorder. Qed.
+
+Hint Extern 3 (PartialOrder (inverse _)) => class_apply PartialOrder_inverse : typeclass_instances.
diff --git a/theories/Classes/RelationPairs.v b/theories/Classes/RelationPairs.v
new file mode 100644
index 00000000..7972c96c
--- /dev/null
+++ b/theories/Classes/RelationPairs.v
@@ -0,0 +1,153 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
+
+(** * Relations over pairs *)
+
+
+Require Import Relations Morphisms.
+
+(* NB: This should be system-wide someday, but for that we need to
+    fix the simpl tactic, since "simpl fst" would be refused for
+    the moment.
+
+Implicit Arguments fst [[A] [B]].
+Implicit Arguments snd [[A] [B]].
+Implicit Arguments pair [[A] [B]].
+
+/NB *)
+
+Local Notation Fst := (@fst _ _).
+Local Notation Snd := (@snd _ _).
+
+Arguments Scope relation_conjunction
+ [type_scope signature_scope signature_scope].
+Arguments Scope relation_equivalence
+ [type_scope signature_scope signature_scope].
+Arguments Scope subrelation [type_scope signature_scope signature_scope].
+Arguments Scope Reflexive [type_scope signature_scope].
+Arguments Scope Irreflexive [type_scope signature_scope].
+Arguments Scope Symmetric [type_scope signature_scope].
+Arguments Scope Transitive [type_scope signature_scope].
+Arguments Scope PER [type_scope signature_scope].
+Arguments Scope Equivalence [type_scope signature_scope].
+Arguments Scope StrictOrder [type_scope signature_scope].
+
+Generalizable Variables A B RA RB Ri Ro f.
+
+(** Any function from [A] to [B] allow to obtain a relation over [A]
+    out of a relation over [B]. *)
+
+Definition RelCompFun {A B}(R:relation B)(f:A->B) : relation A :=
+ fun a a' => R (f a) (f a').
+
+Infix "@@" := RelCompFun (at level 30, right associativity) : signature_scope.
+
+Notation "R @@1" := (R @@ Fst)%signature (at level 30) : signature_scope.
+Notation "R @@2" := (R @@ Snd)%signature (at level 30) : signature_scope.
+
+(** We declare measures to the system using the [Measure] class.
+   Otherwise the instances would easily introduce loops,
+   never instantiating the [f] function.  *)
+
+Class Measure {A B} (f : A -> B).
+
+(** Standard measures. *)
+
+Instance fst_measure : @Measure (A * B) A Fst.
+Instance snd_measure : @Measure (A * B) B Snd.
+
+(** We define a product relation over [A*B]: each components should
+    satisfy the corresponding initial relation. *)
+
+Definition RelProd {A B}(RA:relation A)(RB:relation B) : relation (A*B) :=
+ relation_conjunction (RA @@1) (RB @@2).
+
+Infix "*" := RelProd : signature_scope.
+
+Section RelCompFun_Instances.
+  Context {A B : Type} (R : relation B).
+
+  Global Instance RelCompFun_Reflexive
+    `(Measure A B f, Reflexive _ R) : Reflexive (R@@f).
+  Proof. firstorder. Qed.
+
+  Global Instance RelCompFun_Symmetric
+    `(Measure A B f, Symmetric _ R) : Symmetric (R@@f).
+  Proof. firstorder. Qed.
+
+  Global Instance RelCompFun_Transitive
+    `(Measure A B f, Transitive _ R) : Transitive (R@@f).
+  Proof. firstorder. Qed.
+
+  Global Instance RelCompFun_Irreflexive
+    `(Measure A B f, Irreflexive _ R) : Irreflexive (R@@f).
+  Proof. firstorder. Qed.
+
+  Global Instance RelCompFun_Equivalence
+    `(Measure A B f, Equivalence _ R) : Equivalence (R@@f).
+
+  Global Instance RelCompFun_StrictOrder
+    `(Measure A B f, StrictOrder _ R) : StrictOrder (R@@f).
+
+End RelCompFun_Instances.
+
+Instance RelProd_Reflexive {A B}(RA:relation A)(RB:relation B)
+ `(Reflexive _ RA, Reflexive _ RB) : Reflexive (RA*RB).
+Proof. firstorder. Qed.
+
+Instance RelProd_Symmetric {A B}(RA:relation A)(RB:relation B)
+ `(Symmetric _ RA, Symmetric _ RB) : Symmetric (RA*RB).
+Proof. firstorder. Qed.
+
+Instance RelProd_Transitive {A B}(RA:relation A)(RB:relation B)
+ `(Transitive _ RA, Transitive _ RB) : Transitive (RA*RB).
+Proof. firstorder. Qed.
+
+Instance RelProd_Equivalence {A B}(RA:relation A)(RB:relation B)
+ `(Equivalence _ RA, Equivalence _ RB) : Equivalence (RA*RB).
+
+Lemma FstRel_ProdRel {A B}(RA:relation A) :
+ relation_equivalence (RA @@1) (RA*(fun _ _ : B => True)).
+Proof. firstorder. Qed.
+
+Lemma SndRel_ProdRel {A B}(RB:relation B) :
+ relation_equivalence (RB @@2) ((fun _ _ : A =>True) * RB).
+Proof. firstorder. Qed.
+
+Instance FstRel_sub {A B} (RA:relation A)(RB:relation B):
+ subrelation (RA*RB) (RA @@1).
+Proof. firstorder. Qed.
+
+Instance SndRel_sub {A B} (RA:relation A)(RB:relation B):
+ subrelation (RA*RB) (RB @@2).
+Proof. firstorder. Qed.
+
+Instance pair_compat { A B } (RA:relation A)(RB:relation B) :
+ Proper (RA==>RB==> RA*RB) (@pair _ _).
+Proof. firstorder. Qed.
+
+Instance fst_compat { A B } (RA:relation A)(RB:relation B) :
+ Proper (RA*RB ==> RA) Fst.
+Proof.
+intros (x,y) (x',y') (Hx,Hy); compute in *; auto.
+Qed.
+
+Instance snd_compat { A B } (RA:relation A)(RB:relation B) :
+ Proper (RA*RB ==> RB) Snd.
+Proof.
+intros (x,y) (x',y') (Hx,Hy); compute in *; auto.
+Qed.
+
+Instance RelCompFun_compat {A B}(f:A->B)(R : relation B)
+ `(Proper _ (Ri==>Ri==>Ro) R) :
+ Proper (Ri@@f==>Ri@@f==>Ro) (R@@f)%signature.
+Proof. unfold RelCompFun; firstorder. Qed.
+
+Hint Unfold RelProd RelCompFun.
+Hint Extern 2 (RelProd _ _ _ _) => split.
+
diff --git a/theories/Classes/SetoidAxioms.v b/theories/Classes/SetoidAxioms.v
deleted file mode 100644
index 03bb9a80..00000000
--- a/theories/Classes/SetoidAxioms.v
+++ /dev/null
@@ -1,34 +0,0 @@
-(************************************************************************)
-(*  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        *)
-(************************************************************************)
-
-(* Extensionality axioms that can be used when reasoning with setoids.
- *
- * Author: Matthieu Sozeau
- * Institution: LRI, CNRS UMR 8623 - Universit脙copyright Paris Sud
- *              91405 Orsay, France *)
-
-(* $Id: SetoidAxioms.v 12083 2009-04-14 07:22:18Z herbelin $ *)
-
-Require Import Coq.Program.Program.
-
-Set Implicit Arguments.
-Unset Strict Implicit.
-
-Require Export Coq.Classes.SetoidClass.
-
-(* Application of the extensionality axiom to turn a goal on 
-   Leibniz equality to a setoid equivalence (use with care!). *)
-
-Axiom setoideq_eq : forall `{sa : Setoid a} (x y : a), x == y -> x = y.
-
-(** Application of the extensionality principle for setoids. *)
-
-Ltac setoid_extensionality :=
-  match goal with
-    [ |- @eq ?A ?X ?Y ] => apply (setoideq_eq (a:=A) (x:=X) (y:=Y))
-  end.
diff --git a/theories/Classes/SetoidClass.v b/theories/Classes/SetoidClass.v
index d3da7d5a..c41c5769 100644
--- a/theories/Classes/SetoidClass.v
+++ b/theories/Classes/SetoidClass.v
@@ -6,23 +6,24 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* Typeclass-based setoids, tactics and standard instances.
- 
+(** * Typeclass-based setoids, tactics and standard instances.
+
    Author: Matthieu Sozeau
-   Institution: LRI, CNRS UMR 8623 - Universit胏opyright Paris Sud
-   91405 Orsay, France *)
+   Institution: LRI, CNRS UMR 8623 - University Paris Sud
+*)
 
-(* $Id: SetoidClass.v 12187 2009-06-13 19:36:59Z msozeau $ *)
+(* $Id$ *)
 
 Set Implicit Arguments.
 Unset Strict Implicit.
 
+Generalizable Variables A.
+
 Require Import Coq.Program.Program.
 
 Require Import Relation_Definitions.
 Require Export Coq.Classes.RelationClasses.
 Require Export Coq.Classes.Morphisms.
-Require Import Coq.Classes.Functions.
 
 (** A setoid wraps an equivalence. *)
 
@@ -55,7 +56,7 @@ Existing Instance setoid_trans.
 (* Program Instance eq_setoid : Setoid A := *)
 (*   equiv := eq ; setoid_equiv := eq_equivalence. *)
 
-Program Instance iff_setoid : Setoid Prop := 
+Program Instance iff_setoid : Setoid Prop :=
   { equiv := iff ; setoid_equiv := iff_equivalence }.
 
 (** Overloaded notations for setoid equivalence and inequivalence. Not to be confused with [eq] and [=]. *)
@@ -69,7 +70,7 @@ Notation " x =/= y " := (complement equiv x y) (at level 70, no associativity) :
 
 (** Use the [clsubstitute] command which substitutes an equality in every hypothesis. *)
 
-Ltac clsubst H := 
+Ltac clsubst H :=
   match type of H with
     ?x == ?y => substitute H ; clear H x
   end.
@@ -79,7 +80,7 @@ Ltac clsubst_nofail :=
     | [ H : ?x == ?y |- _ ] => clsubst H ; clsubst_nofail
     | _ => idtac
   end.
-  
+
 (** [subst*] will try its best at substituting every equality in the goal. *)
 
 Tactic Notation "clsubst" "*" := clsubst_nofail.
@@ -94,7 +95,7 @@ Qed.
 
 Lemma equiv_nequiv_trans : forall `{Setoid A} (x y z : A), x == y -> y =/= z -> x =/= z.
 Proof.
-  intros; intro. 
+  intros; intro.
   assert(y == x) by (symmetry ; auto).
   assert(y == z) by (transitivity x ; eauto).
   contradiction.
@@ -119,25 +120,15 @@ Ltac setoidify := repeat setoidify_tac.
 
 (** Every setoid relation gives rise to a morphism, in fact every partial setoid does. *)
 
-Program Instance setoid_morphism `(sa : Setoid A) : Morphism (equiv ++> equiv ++> iff) equiv :=
-  respect.
-
-Program Instance setoid_partial_app_morphism `(sa : Setoid A) (x : A) : Morphism (equiv ++> iff) (equiv x) :=
-  respect.
-
-Ltac morphism_tac := try red ; unfold arrow ; intros ; program_simpl ; try tauto.
-
-Ltac obligation_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 setoid_morphism `(sa : Setoid A) : Proper (equiv ++> equiv ++> iff) equiv :=
+  proper_prf.
 
-Program Instance iff_impl_id_morphism : Morphism (iff ++> impl) id.
+Program Instance setoid_partial_app_morphism `(sa : Setoid A) (x : A) : Proper (equiv ++> iff) (equiv x) :=
+  proper_prf.
 
 (** Partial setoids don't require reflexivity so we can build a partial setoid on the function space. *)
 
-Class PartialSetoid (A : Type) := 
+Class PartialSetoid (A : Type) :=
   { pequiv : relation A ; pequiv_prf :> PER pequiv }.
 
 (** Overloaded notation for partial setoid equivalence. *)
@@ -146,4 +137,4 @@ Infix "=~=" := pequiv (at level 70, no associativity) : type_scope.
 
 (** Reset the default Program tactic. *)
 
-Ltac obligation_tactic ::= program_simpl.
+Obligation Tactic := program_simpl.
diff --git a/theories/Classes/SetoidDec.v b/theories/Classes/SetoidDec.v
index bac64724..33b4350f 100644
--- a/theories/Classes/SetoidDec.v
+++ b/theories/Classes/SetoidDec.v
@@ -1,3 +1,4 @@
+(* -*- coding: utf-8 -*- *)
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
 (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
@@ -6,43 +7,47 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* Decidable setoid equality theory.
- *
- * Author: Matthieu Sozeau
- * Institution: LRI, CNRS UMR 8623 - Universit脙copyright Paris Sud
- *              91405 Orsay, France *)
+(** * Decidable setoid equality theory.
 
-(* $Id: SetoidDec.v 11800 2009-01-18 18:34:15Z msozeau $ *)
+   Author: Matthieu Sozeau
+   Institution: LRI, CNRS UMR 8623 - University Paris Sud
+*)
+
+(* $Id$ *)
 
 Set Implicit Arguments.
 Unset Strict Implicit.
 
+Generalizable Variables A B .
+
 (** Export notations. *)
 
 Require Export Coq.Classes.SetoidClass.
 
-(** The [DecidableSetoid] class asserts decidability of a [Setoid]. It can be useful in proofs to reason more 
-   classically. *)
+(** The [DecidableSetoid] class asserts decidability of a [Setoid].
+   It can be useful in proofs to reason more classically. *)
 
 Require Import Coq.Logic.Decidable.
 
 Class DecidableSetoid `(S : Setoid A) :=
   setoid_decidable : forall x y : A, decidable (x == y).
 
-(** The [EqDec] class gives a decision procedure for a particular setoid equality. *)
+(** The [EqDec] class gives a decision procedure for a particular setoid
+   equality. *)
 
 Class EqDec `(S : Setoid A) :=
   equiv_dec : forall x y : A, { x == y } + { x =/= y }.
 
-(** We define the [==] overloaded notation for deciding equality. It does not take precedence
-   of [==] defined in the type scope, hence we can have both at the same time. *)
+(** We define the [==] overloaded notation for deciding equality. It does not
+   take precedence of [==] defined in the type scope, hence we can have both
+   at the same time. *)
 
 Notation " x == y " := (equiv_dec (x :>) (y :>)) (no associativity, at level 70).
 
 Definition swap_sumbool {A B} (x : { A } + { B }) : { B } + { A } :=
   match x with
-    | left H => @right _ _ H 
-    | right H => @left _ _ H 
+    | left H => @right _ _ H
+    | right H => @left _ _ H
   end.
 
 Require Import Coq.Program.Program.
@@ -72,7 +77,8 @@ Infix "<>b" := nequiv_decb (no associativity, at level 70).
 
 Require Import Coq.Arith.Arith.
 
-(** The equiv is burried inside the setoid, but we can recover it by specifying which setoid we're talking about. *)
+(** The equiv is burried inside the setoid, but we can recover
+  it by specifying which setoid we're talking about. *)
 
 Program Instance eq_setoid A : Setoid A | 10 :=
   { equiv := eq ; setoid_equiv := eq_equivalence }.
@@ -96,16 +102,17 @@ Program Instance unit_eqdec : EqDec (eq_setoid unit) :=
 
 Program Instance prod_eqdec `(! EqDec (eq_setoid A), ! EqDec (eq_setoid B)) : EqDec (eq_setoid (prod A B)) :=
   位 x y,
-    let '(x1, x2) := x in 
-    let '(y1, y2) := y in 
-    if x1 == y1 then 
+    let '(x1, x2) := x in
+    let '(y1, y2) := y in
+    if x1 == y1 then
       if x2 == y2 then in_left
       else in_right
     else in_right.
 
   Solve Obligations using unfold complement ; program_simpl.
 
-(** Objects of function spaces with countable domains like bool have decidable equality. *)
+(** Objects of function spaces with countable domains like bool
+  have decidable equality. *)
 
 Program Instance bool_function_eqdec `(! EqDec (eq_setoid A)) : EqDec (eq_setoid (bool -> A)) :=
   位 f g,
diff --git a/theories/Classes/SetoidTactics.v b/theories/Classes/SetoidTactics.v
index 36f05e31..669be8b0 100644
--- a/theories/Classes/SetoidTactics.v
+++ b/theories/Classes/SetoidTactics.v
@@ -1,4 +1,3 @@
-(* -*- coq-prog-args: ("-emacs-U" "-top" "Coq.Classes.SetoidTactics") -*- *)
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
 (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
@@ -7,38 +6,28 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* Tactics for typeclass-based setoids.
- *
- * Author: Matthieu Sozeau
- * Institution: LRI, CNRS UMR 8623 - Universit胏opyright Paris Sud
- *              91405 Orsay, France *)
+(** * Tactics for typeclass-based setoids.
 
-(* $Id: SetoidTactics.v 12187 2009-06-13 19:36:59Z msozeau $ *)
+   Author: Matthieu Sozeau
+   Institution: LRI, CNRS UMR 8623 - University Paris Sud
+*)
+
+(* $Id$ *)
 
 Require Import Coq.Classes.Morphisms Coq.Classes.Morphisms_Prop.
 Require Export Coq.Classes.RelationClasses Coq.Relations.Relation_Definitions.
 Require Import Coq.Classes.Equivalence Coq.Program.Basics.
 
-Export MorphismNotations.
+Generalizable Variables A R.
+
+Export ProperNotations.
 
 Set Implicit Arguments.
 Unset Strict Implicit.
 
-(** Setoid relation on a given support: declares a relation as a setoid
-   for use with rewrite. It helps choosing if a rewrite should be handled
-   by setoid_rewrite or the regular rewrite using leibniz equality.
-   Users can declare an [SetoidRelation A RA] anywhere to declare default 
-   relations. This is also done automatically by the [Declare Relation A RA]
-   commands. *)
-
-Class SetoidRelation A (R : relation A).
-
-Instance impl_setoid_relation : SetoidRelation impl.
-Instance iff_setoid_relation : SetoidRelation iff.
-
 (** Default relation on a given support. Can be used by tactics
-   to find a sensible default relation on any carrier. Users can 
-   declare an [Instance def : DefaultRelation A RA] anywhere to 
+   to find a sensible default relation on any carrier. Users can
+   declare an [Instance def : DefaultRelation A RA] anywhere to
    declare default relations. *)
 
 Class DefaultRelation A (R : relation A).
@@ -47,12 +36,13 @@ Class DefaultRelation A (R : relation A).
 
 Definition default_relation `{DefaultRelation A R} := R.
 
-(** Every [Equivalence] gives a default relation, if no other is given (lowest priority). *)
+(** Every [Equivalence] gives a default relation, if no other is given
+  (lowest priority). *)
 
 Instance equivalence_default `(Equivalence A R) : DefaultRelation R | 4.
 
-(** The setoid_replace tactics in Ltac, defined in terms of default relations and
-   the setoid_rewrite tactic. *)
+(** The setoid_replace tactics in Ltac, defined in terms of default relations
+  and the setoid_rewrite tactic. *)
 
 Ltac setoidreplace H t :=
   let Heq := fresh "Heq" in
@@ -73,86 +63,88 @@ Ltac setoidreplaceat H t occs :=
 Tactic Notation "setoid_replace" constr(x) "with" constr(y) :=
   setoidreplace (default_relation x y) idtac.
 
-Tactic Notation "setoid_replace" constr(x) "with" constr(y) 
+Tactic Notation "setoid_replace" constr(x) "with" constr(y)
   "at" int_or_var_list(o) :=
   setoidreplaceat (default_relation x y) idtac o.
 
-Tactic Notation "setoid_replace" constr(x) "with" constr(y) 
+Tactic Notation "setoid_replace" constr(x) "with" constr(y)
   "in" hyp(id) :=
   setoidreplacein (default_relation x y) id idtac.
 
 Tactic Notation "setoid_replace" constr(x) "with" constr(y)
-  "in" hyp(id) 
+  "in" hyp(id)
   "at" int_or_var_list(o) :=
   setoidreplaceinat (default_relation x y) id idtac o.
 
-Tactic Notation "setoid_replace" constr(x) "with" constr(y) 
+Tactic Notation "setoid_replace" constr(x) "with" constr(y)
   "by" tactic3(t) :=
   setoidreplace (default_relation x y) ltac:t.
 
-Tactic Notation "setoid_replace" constr(x) "with" constr(y) 
-  "at" int_or_var_list(o) 
+Tactic Notation "setoid_replace" constr(x) "with" constr(y)
+  "at" int_or_var_list(o)
   "by" tactic3(t) :=
   setoidreplaceat (default_relation x y) ltac:t o.
 
-Tactic Notation "setoid_replace" constr(x) "with" constr(y) 
-  "in" hyp(id) 
+Tactic Notation "setoid_replace" constr(x) "with" constr(y)
+  "in" hyp(id)
   "by" tactic3(t) :=
   setoidreplacein (default_relation x y) id ltac:t.
 
-Tactic Notation "setoid_replace" constr(x) "with" constr(y) 
-  "in" hyp(id) 
-  "at" int_or_var_list(o) 
+Tactic Notation "setoid_replace" constr(x) "with" constr(y)
+  "in" hyp(id)
+  "at" int_or_var_list(o)
   "by" tactic3(t) :=
   setoidreplaceinat (default_relation x y) id ltac:t o.
 
-Tactic Notation "setoid_replace" constr(x) "with" constr(y) 
+Tactic Notation "setoid_replace" constr(x) "with" constr(y)
   "using" "relation" constr(rel) :=
   setoidreplace (rel x y) idtac.
 
-Tactic Notation "setoid_replace" constr(x) "with" constr(y) 
+Tactic Notation "setoid_replace" constr(x) "with" constr(y)
   "using" "relation" constr(rel)
   "at" int_or_var_list(o) :=
   setoidreplaceat (rel x y) idtac o.
 
-Tactic Notation "setoid_replace" constr(x) "with" constr(y) 
-  "using" "relation" constr(rel) 
+Tactic Notation "setoid_replace" constr(x) "with" constr(y)
+  "using" "relation" constr(rel)
   "by" tactic3(t) :=
   setoidreplace (rel x y) ltac:t.
 
-Tactic Notation "setoid_replace" constr(x) "with" constr(y) 
-  "using" "relation" constr(rel) 
-  "at" int_or_var_list(o)  
+Tactic Notation "setoid_replace" constr(x) "with" constr(y)
+  "using" "relation" constr(rel)
+  "at" int_or_var_list(o)
   "by" tactic3(t) :=
   setoidreplaceat (rel x y) ltac:t o.
 
-Tactic Notation "setoid_replace" constr(x) "with" constr(y) 
+Tactic Notation "setoid_replace" constr(x) "with" constr(y)
   "using" "relation" constr(rel)
   "in" hyp(id) :=
   setoidreplacein (rel x y) id idtac.
 
-Tactic Notation "setoid_replace" constr(x) "with" constr(y) 
+Tactic Notation "setoid_replace" constr(x) "with" constr(y)
   "using" "relation" constr(rel)
-  "in" hyp(id) 
+  "in" hyp(id)
   "at" int_or_var_list(o) :=
   setoidreplaceinat (rel x y) id idtac o.
 
-Tactic Notation "setoid_replace" constr(x) "with" constr(y) 
+Tactic Notation "setoid_replace" constr(x) "with" constr(y)
   "using" "relation" constr(rel)
   "in" hyp(id)
   "by" tactic3(t) :=
   setoidreplacein (rel x y) id ltac:t.
 
-Tactic Notation "setoid_replace" constr(x) "with" constr(y) 
-  "using" "relation" constr(rel) 
+Tactic Notation "setoid_replace" constr(x) "with" constr(y)
+  "using" "relation" constr(rel)
   "in" hyp(id)
-  "at" int_or_var_list(o)  
+  "at" int_or_var_list(o)
   "by" tactic3(t) :=
   setoidreplaceinat (rel x y) id ltac:t o.
 
-(** The [add_morphism_tactic] tactic is run at each [Add Morphism] command before giving the hand back
-   to the user to discharge the proof. It essentially amounts to unfold the right amount of [respectful] calls
-   and substitute leibniz equalities. One can redefine it using [Ltac add_morphism_tactic ::= t]. *)
+(** The [add_morphism_tactic] tactic is run at each [Add Morphism]
+   command before giving the hand back to the user to discharge the
+   proof. It essentially amounts to unfold the right amount of
+   [respectful] calls and substitute leibniz equalities. One can
+   redefine it using [Ltac add_morphism_tactic ::= t]. *)
 
 Require Import Coq.Program.Tactics.
 
@@ -165,9 +157,9 @@ Ltac red_subst_eq_morphism concl :=
     | _ => idtac
   end.
 
-Ltac destruct_morphism :=
+Ltac destruct_proper :=
   match goal with
-    | [ |- @Morphism ?A ?R ?m ] => red
+    | [ |- @Proper ?A ?R ?m ] => red
   end.
 
 Ltac reverse_arrows x :=
@@ -179,11 +171,13 @@ Ltac reverse_arrows x :=
 
 Ltac default_add_morphism_tactic :=
   unfold flip ; intros ;
-  (try destruct_morphism) ;
+  (try destruct_proper) ;
   match goal with
     | [ |- (?x ==> ?y) _ _ ] => red_subst_eq_morphism (x ==> y) ; reverse_arrows (x ==> y)
   end.
 
 Ltac add_morphism_tactic := default_add_morphism_tactic.
 
-Ltac obligation_tactic ::= program_simpl.
+Obligation Tactic := program_simpl.
+
+(* Notation "'Morphism' s t " := (@Proper _ (s%signature) t) (at level 10, s at next level, t at next level). *)
diff --git a/theories/Classes/vo.itarget b/theories/Classes/vo.itarget
new file mode 100644
index 00000000..9daf133b
--- /dev/null
+++ b/theories/Classes/vo.itarget
@@ -0,0 +1,11 @@
+Equivalence.vo
+EquivDec.vo
+Init.vo
+Morphisms_Prop.vo
+Morphisms_Relations.vo
+Morphisms.vo
+RelationClasses.vo
+SetoidClass.vo
+SetoidDec.vo
+SetoidTactics.vo
+RelationPairs.vo