Imported Upstream version 8.5~beta1+dfsg

16 files changed, 1939 insertions, 614 deletions

diff --git a/theories/Classes/CEquivalence.v b/theories/Classes/CEquivalence.v
new file mode 100644
index 00000000..65353ed2
--- /dev/null
+++ b/theories/Classes/CEquivalence.v
@@ -0,0 +1,139 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(** * Typeclass-based setoids. Definitions on [Equivalence].
+
+   Author: Matthieu Sozeau
+   Institution: LRI, CNRS UMR 8623 - University Paris Sud
+*)
+
+Require Import Coq.Program.Basics.
+Require Import Coq.Program.Tactics.
+
+Require Import Coq.Classes.Init.
+Require Import Relation_Definitions.
+Require Export Coq.Classes.CRelationClasses.
+Require Import Coq.Classes.CMorphisms.
+
+Set Implicit Arguments.
+Unset Strict Implicit.
+
+Generalizable Variables A R eqA B S eqB.
+Local Obligation Tactic := try solve [simpl_crelation].
+
+Local Open Scope signature_scope.
+
+Definition equiv `{Equivalence A R} : crelation A := R.
+
+(** 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.
+
+Local Open Scope equiv_scope.
+
+(** Overloading for [PER]. *)
+
+Definition pequiv `{PER A R} : crelation A := R.
+
+(** Overloaded notation for partial equivalence. *)
+
+Infix "=~=" := pequiv (at level 70, no associativity) : equiv_scope.
+
+(** Shortcuts to make proof search easier. *)
+
+Program Instance equiv_reflexive `(sa : Equivalence A) : Reflexive equiv.
+
+Program Instance equiv_symmetric `(sa : Equivalence A) : Symmetric equiv.
+
+Program Instance equiv_transitive `(sa : Equivalence A) : Transitive equiv.
+
+  Next Obligation.
+  Proof. intros A R sa x y z Hxy Hyz.
+         now transitivity y.
+  Qed.
+
+(** Use the [substitute] command which substitutes an equivalence 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.
+
+(** Simplify the goal w.r.t. equivalence. *)
+
+Ltac equiv_simplify_one :=
+  match goal with
+    | [ H : ?x === ?x |- _ ] => clear H
+    | [ H : ?x === ?y |- _ ] => setoid_subst H
+    | [ |- ?x =/= ?y ] => let name:=fresh "Hneq" in intro name
+    | [ |- ~ ?x === ?y ] => let name:=fresh "Hneq" in intro name
+  end.
+
+Ltac equiv_simplify := repeat equiv_simplify_one.
+
+(** "reify" relations which are equivalences to applications of the overloaded [equiv] method
+   for easy recognition in tactics. *)
+
+Ltac equivify_tac :=
+  match goal with
+    | [ s : Equivalence ?A ?R, H : ?R ?x ?y |- _ ] => change R with (@equiv A R s) in H
+    | [ s : Equivalence ?A ?R |- context C [ ?R ?x ?y ] ] => change (R x y) with (@equiv A R s x y)
+  end.
+
+Ltac equivify := repeat equivify_tac.
+
+Section Respecting.
+
+  (** Here we build an equivalence instance for functions which relates respectful ones only,
+     we do not export it. *)
+
+  Definition respecting `(eqa : Equivalence A (R : crelation A), 
+                          eqb : Equivalence B (R' : crelation 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' (projT1 f x) (projT1 g y)).
+
+  Solve Obligations with unfold respecting in * ; simpl_crelation ; program_simpl.
+
+  Next Obligation.
+  Proof. 
+    intros. intros f g h H H' x y Rxy.
+    unfold respecting in *. program_simpl. transitivity (g y); auto. firstorder.
+  Qed.
+
+End Respecting.
+
+(** The default equivalence on function spaces, with higher-priority than [eq]. *)
+
+Instance pointwise_reflexive {A} `(reflb : Reflexive B eqB) :
+  Reflexive (pointwise_relation A eqB) | 9.
+Proof. firstorder. Qed.
+Instance pointwise_symmetric {A} `(symb : Symmetric B eqB) :
+  Symmetric (pointwise_relation A eqB) | 9.
+Proof. firstorder. Qed.
+Instance pointwise_transitive {A} `(transb : Transitive B eqB) :
+  Transitive (pointwise_relation A eqB) | 9.
+Proof. firstorder. Qed.
+Instance pointwise_equivalence {A} `(eqb : Equivalence B eqB) :
+  Equivalence (pointwise_relation A eqB) | 9.
+Proof. split; apply _. Qed.
diff --git a/theories/Classes/CMorphisms.v b/theories/Classes/CMorphisms.v
new file mode 100644
index 00000000..073cd5e9
--- /dev/null
+++ b/theories/Classes/CMorphisms.v
@@ -0,0 +1,701 @@
+(* -*- coding: utf-8 -*- *)
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(** * Typeclass-based morphism definition and standard, minimal instances
+
+   Author: Matthieu Sozeau
+   Institution: LRI, CNRS UMR 8623 - University Paris Sud
+*)
+
+Require Import Coq.Program.Basics.
+Require Import Coq.Program.Tactics.
+Require Export Coq.Classes.CRelationClasses.
+
+Generalizable Variables A eqA B C D R RA RB RC m f x y.
+Local Obligation Tactic := simpl_crelation.
+
+Set Universe Polymorphism.
+
+(** * Morphisms.
+
+   We now turn to the definition of [Proper] and declare standard instances.
+   These will be used by the [setoid_rewrite] tactic later. *)
+
+(** 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. *)
+Section Proper.
+  Context {A B : Type}.
+
+  Class Proper (R : crelation A) (m : A) :=
+    proper_prf : R m m.
+
+  (** 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 [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. *)
+
+  Class ProperProxy (R : crelation A) (m : A) :=
+    proper_proxy : R m m.
+
+  Lemma eq_proper_proxy (x : A) : ProperProxy (@eq A) x.
+  Proof. firstorder. Qed.
+  
+  Lemma reflexive_proper_proxy `(Reflexive A R) (x : A) : ProperProxy R x.
+  Proof. firstorder. Qed.
+
+  Lemma proper_proper_proxy x `(Proper R x) : ProperProxy R x.
+  Proof. firstorder. Qed.
+
+  (** Respectful morphisms. *)
+  
+  (** The fully dependent version, not used yet. *)
+  
+  Definition respectful_hetero
+  (A B : Type)
+  (C : A -> Type) (D : B -> Type)
+  (R : A -> B -> Type)
+  (R' : forall (x : A) (y : B), C x -> D y -> Type) :
+    (forall x : A, C x) -> (forall x : B, D x) -> Type :=
+    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. *)
+  
+  Definition respectful (R : crelation A) (R' : crelation B) : crelation (A -> B) :=
+    Eval compute in @respectful_hetero A A (fun _ => B) (fun _ => B) R (fun _ _ => R').
+End Proper.
+
+(** We favor the use of Leibniz equality or a declared reflexive crelation 
+  when resolving [ProperProxy], otherwise, if the crelation is given (not an evar),
+  we fall back to [Proper]. *)
+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.
+
+(** Notations reminiscent of the old syntax for declaring morphisms. *)
+Delimit Scope signature_scope with signature.
+
+Module ProperNotations.
+
+  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 _ _ (flip (R%signature)) (R'%signature))
+    (right associativity, at level 55) : signature_scope.
+
+End ProperNotations.
+
+Arguments Proper {A}%type R%signature m.
+Arguments respectful {A B}%type (R R')%signature _ _.
+
+Export ProperNotations.
+
+Local Open Scope signature_scope.
+
+(** [solve_proper] try to solve the goal [Proper (?==> ... ==>?) f]
+    by repeated introductions and setoid rewrites. It should work
+    fine when [f] is a combination of already known morphisms and
+    quantifiers. *)
+
+Ltac solve_respectful t :=
+ match goal with
+   | |- respectful _ _ _ _ =>
+     let H := fresh "H" in
+     intros ? ? H; solve_respectful ltac:(setoid_rewrite H; t)
+   | _ => t; reflexivity
+ end.
+
+Ltac solve_proper := unfold Proper; solve_respectful ltac:(idtac).
+
+(** [f_equiv] is a clone of [f_equal] that handles setoid equivalences.
+    For example, if we know that [f] is a morphism for [E1==>E2==>E],
+    then the goal [E (f x y) (f x' y')] will be transformed by [f_equiv]
+    into the subgoals [E1 x x'] and [E2 y y'].
+*)
+
+Ltac f_equiv :=
+ match goal with
+  | |- ?R (?f ?x) (?f' _) =>
+    let T := type of x in
+    let Rx := fresh "R" in
+    evar (Rx : crelation T);
+    let H := fresh in
+    assert (H : (Rx==>R)%signature f f');
+    unfold Rx in *; clear Rx; [ f_equiv | apply H; clear H; try reflexivity ]
+  | |- ?R ?f ?f' =>
+    solve [change (Proper R f); eauto with typeclass_instances | reflexivity ]
+  | _ => idtac
+ end.
+
+Section Relations.
+  Context {A B : Type}. 
+
+  (** [forall_def] reifies the dependent product as a definition. *)
+  
+  Definition forall_def (P : A -> Type) : Type := forall x : A, P x.
+  
+  (** Dependent pointwise lifting of a crelation on the range. *)
+  
+  Definition forall_relation (P : A -> Type)
+             (sig : forall a, crelation (P a)) : crelation (forall x, P x) :=
+    fun f g => forall a, sig a (f a) (g a).
+
+  (** Non-dependent pointwise lifting *)
+  Definition pointwise_relation (R : crelation B) : crelation (A -> B) :=
+    fun f g => forall a, R (f a) (g a).
+
+  Lemma pointwise_pointwise (R : crelation B) :
+    relation_equivalence (pointwise_relation R) (@eq A ==> R).
+  Proof. intros. split. simpl_crelation. firstorder. Qed.
+  
+  (** Subcrelations induce a morphism on the identity. *)
+  
+  Global Instance subrelation_id_proper `(subrelation A RA RA') : Proper (RA ==> RA') id.
+  Proof. firstorder. Qed.
+
+  (** The subrelation property goes through products as usual. *)
+  
+  Lemma subrelation_respectful `(subl : subrelation A RA' RA, subr : subrelation B RB RB') :
+    subrelation (RA ==> RB) (RA' ==> RB').
+  Proof. simpl_crelation. Qed.
+
+  (** And of course it is reflexive. *)
+  
+  Lemma subrelation_refl R : @subrelation A R R.
+  Proof. simpl_crelation. Qed.
+
+  (** [Proper] is itself a covariant morphism for [subrelation].
+   We use an unconvertible premise to avoid looping.
+   *)
+  
+  Lemma subrelation_proper `(mor : Proper A R' m) 
+        `(unc : Unconvertible (crelation A) R R')
+        `(sub : subrelation A R' R) : Proper R m.
+  Proof.
+    intros. apply sub. apply mor.
+  Qed.
+
+  Global Instance proper_subrelation_proper_arrow :
+    Proper (subrelation ++> eq ==> arrow) (@Proper A).
+  Proof. reduce. subst. firstorder. Qed.
+
+  Global Instance pointwise_subrelation `(sub : subrelation B R R') :
+    subrelation (pointwise_relation R) (pointwise_relation R') | 4.
+  Proof. reduce. unfold pointwise_relation in *. apply sub. auto. Qed.
+  
+  (** For dependent function types. *)
+  Lemma forall_subrelation (P : A -> Type) (R S : forall x : A, crelation (P x)) :
+    (forall a, subrelation (R a) (S a)) -> 
+    subrelation (forall_relation P R) (forall_relation P S).
+  Proof. reduce. firstorder. Qed.
+End Relations.
+Typeclasses Opaque respectful pointwise_relation forall_relation.
+Arguments forall_relation {A P}%type sig%signature _ _.
+Arguments pointwise_relation A%type {B}%type R%signature _ _.
+  
+Hint Unfold Reflexive : core.
+Hint Unfold Symmetric : core.
+Hint Unfold Transitive : core.
+
+(** Resolution with subrelation: favor decomposing products over applying reflexivity
+  for unconstrained goals. *)
+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.
+
+CoInductive apply_subrelation : Prop := do_subrelation.
+
+Ltac proper_subrelation :=
+  match goal with
+    [ H : apply_subrelation |- _ ] => clear H ; class_apply @subrelation_proper
+  end.
+
+Hint Extern 5 (@Proper _ ?H _) => proper_subrelation : typeclass_instances.
+
+(** Essential subrelation instances for [iff], [impl] and [pointwise_relation]. *)
+
+Instance iff_impl_subrelation : subrelation iff impl | 2.
+Proof. firstorder. Qed.
+
+Instance iff_flip_impl_subrelation : subrelation iff (flip impl) | 2.
+Proof. firstorder. Qed.
+
+(** Essential subrelation instances for [iffT] and [arrow]. *)
+
+Instance iffT_arrow_subrelation : subrelation iffT arrow | 2.
+Proof. firstorder. Qed.
+
+Instance iffT_flip_arrow_subrelation : subrelation iffT (flip arrow) | 2.
+Proof. firstorder. 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.
+
+Section GenericInstances.
+  (* Share universes *)
+  Context {A B C : Type}.
+
+  (** We can build a PER on the Coq function space if we have PERs on the domain and
+   codomain. *)
+  
+  Program Instance respectful_per `(PER A R, PER B R') : PER (R ==> R').
+
+  Next Obligation.
+  Proof with auto.
+    assert(R x0 x0).
+    transitivity y0... symmetry...
+    transitivity (y x0)...
+  Qed.
+
+  (** The complement of a crelation conserves its proper elements. *)
+  
+  Program Definition complement_proper
+          `(mR : Proper (A -> A -> Prop) (RA ==> RA ==> iff) R) :
+    Proper (RA ==> RA ==> iff) (complement R) := _.
+  
+  Next Obligation.
+  Proof.
+    unfold complement.
+    pose (mR x y X x0 y0 X0).
+    intuition.
+  Qed.
+ 
+  (** The [flip] too, actually the [flip] instance is a bit more general. *)
+
+  Program Definition 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 crelation gives rise to a binary morphism on [impl],
+   contravariant in the first argument, covariant in the second. *)
+  
+  Global Program 
+  Instance trans_contra_co_type_morphism
+    `(Transitive A R) : Proper (R --> R ++> arrow) R.
+  
+  Next Obligation.
+  Proof with auto.
+    transitivity x...
+    transitivity x0...
+  Qed.
+
+  (** Proper declarations for partial applications. *)
+
+  Global Program 
+  Instance trans_contra_inv_impl_type_morphism
+  `(Transitive A R) : Proper (R --> flip arrow) (R x) | 3.
+
+  Next Obligation.
+  Proof with auto.
+    transitivity y...
+  Qed.
+
+  Global Program 
+  Instance trans_co_impl_type_morphism
+    `(Transitive A R) : Proper (R ++> arrow) (R x) | 3.
+
+  Next Obligation.
+  Proof with auto.
+    transitivity x0...
+  Qed.
+
+  Global Program 
+  Instance trans_sym_co_inv_impl_type_morphism
+    `(PER A R) : Proper (R ++> flip arrow) (R x) | 3.
+
+  Next Obligation.
+  Proof with auto.
+    transitivity y... symmetry...
+  Qed.
+
+  Global Program Instance trans_sym_contra_arrow_morphism
+    `(PER A R) : Proper (R --> arrow) (R x) | 3.
+
+  Next Obligation.
+  Proof with auto.
+    transitivity x0... symmetry...
+  Qed.
+
+  Global Program Instance per_partial_app_type_morphism
+  `(PER A R) : Proper (R ==> iffT) (R x) | 2.
+
+  Next Obligation.
+  Proof with auto.
+    split. intros ; transitivity x0...
+    intros.
+    transitivity y...
+    symmetry...
+  Qed.
+
+  (** Every Transitive crelation induces a morphism by "pushing" an [R x y] on the left of an [R x z] proof to get an [R y z] goal. *)
+
+  Global Program 
+  Instance trans_co_eq_inv_arrow_morphism
+  `(Transitive A R) : Proper (R ==> (@eq A) ==> flip arrow) R | 2.
+
+  Next Obligation.
+  Proof with auto.
+    transitivity y...
+  Qed.
+
+  (** Every Symmetric and Transitive crelation gives rise to an equivariant morphism. *)
+
+  Global Program 
+  Instance PER_type_morphism `(PER A R) : Proper (R ==> R ==> iffT) R | 1.
+
+  Next Obligation.
+  Proof with auto.
+    split ; intros.
+    transitivity x0... transitivity x... symmetry...
+
+    transitivity y... transitivity y0... symmetry...
+  Qed.
+
+  Lemma symmetric_equiv_flip `(Symmetric A R) : relation_equivalence R (flip R).
+  Proof. firstorder. Qed.
+
+  Global Program Instance compose_proper RA RB RC :
+    Proper ((RB ==> RC) ==> (RA ==> RB) ==> (RA ==> RC)) (@compose A B C).
+
+  Next Obligation.
+  Proof.
+    simpl_crelation.
+    unfold compose. firstorder. 
+  Qed.
+
+  (** Coq functions are morphisms for Leibniz equality,
+     applied only if really needed. *)
+
+  Global Instance reflexive_eq_dom_reflexive `(Reflexive B R') :
+    Reflexive (@Logic.eq A ==> R').
+  Proof. simpl_crelation. Qed.
+
+  (** [respectful] is a morphism for crelation equivalence . *)
+  Set Printing All. Set Printing Universes.
+  Global Instance respectful_morphism :
+    Proper (relation_equivalence ++> relation_equivalence ++> relation_equivalence) 
+           (@respectful A B).
+  Proof. 
+    intros R R' HRR' S S' HSS' f g. 
+    unfold respectful , relation_equivalence in *; simpl in *.
+    split ; intros H x y Hxy.
+    apply (fst (HSS' _ _)). apply H. now apply (snd (HRR' _ _)). 
+    apply (snd (HSS' _ _)). apply H. now apply (fst (HRR' _ _)). 
+  Qed.
+
+  (** [R] is Reflexive, hence we can build the needed proof. *)
+
+  Lemma Reflexive_partial_app_morphism `(Proper (A -> B) (R ==> R') m, ProperProxy A R x) :
+    Proper R' (m x).
+  Proof. simpl_crelation. Qed.
+  
+  Class Params (of : A) (arity : nat).
+    
+  Lemma flip_respectful (R : crelation A) (R' : crelation B) :
+    relation_equivalence (flip (R ==> R')) (flip R ==> flip R').
+  Proof.
+    intros.
+    unfold flip, respectful.
+    split ; intros ; intuition.
+  Qed.
+
+  
+  (** Treating flip: can't make them direct instances as we
+   need at least a [flip] present in the goal. *)
+  
+  Lemma flip1 `(subrelation A R' R) : subrelation (flip (flip R')) R.
+  Proof. firstorder. Qed.
+  
+  Lemma flip2 `(subrelation A R R') : subrelation R (flip (flip R')).
+  Proof. firstorder. Qed.
+  
+  (** That's if and only if *)
+  
+  Lemma eq_subrelation `(Reflexive A R) : subrelation (@eq A) R.
+  Proof. simpl_crelation. Qed.
+
+  (** Once we have normalized, we will apply this instance to simplify the problem. *)
+  
+  Definition proper_flip_proper `(mor : Proper A R m) : Proper (flip R) m := mor.
+  
+  (** Every reflexive crelation gives rise to a morphism, 
+  only for immediately solving goals without variables. *)
+  
+  Lemma reflexive_proper `{Reflexive A R} (x : A) : Proper R x.
+  Proof. firstorder. Qed.
+  
+  Lemma proper_eq (x : A) : Proper (@eq A) x.
+  Proof. intros. apply reflexive_proper. Qed.
+  
+End GenericInstances.
+
+Class PartialApplication.
+
+CoInductive normalization_done : Prop := did_normalization.
+
+Ltac partial_application_tactic :=
+  let rec do_partial_apps H m cont := 
+    match m with
+      | ?m' ?x => class_apply @Reflexive_partial_app_morphism ; 
+        [(do_partial_apps H m' ltac:idtac)|clear H]
+      | _ => cont
+    end
+  in
+  let rec do_partial H ar m := 
+    match ar with
+      | 0%nat => do_partial_apps H m ltac:(fail 1)
+      | S ?n' =>
+        match m with
+          ?m' ?x => do_partial H n' m'
+        end
+    end
+  in
+  let params m sk fk :=
+    (let m' := fresh in head_of_constr m' m ;
+     let n := fresh in evar (n:nat) ;
+     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 subst m';
+            (sk H v' || fail 1))
+    || fk
+  in
+  let on_morphism m cont :=
+    params m ltac:(fun H n => do_partial H n m)
+      ltac:(cont)
+  in
+  match goal with
+    | [ _ : normalization_done |- _ ] => fail 1
+    | [ _ : @Params _ _ _ |- _ ] => fail 1
+    | [ |- @Proper ?T _ (?m ?x) ] =>
+      match goal with
+        | [ H : PartialApplication |- _ ] =>
+          class_apply @Reflexive_partial_app_morphism; [|clear H]
+        | _ => on_morphism (m x)
+          ltac:(class_apply @Reflexive_partial_app_morphism)
+      end
+  end.
+
+(** Bootstrap !!! *)
+
+Instance proper_proper : Proper (relation_equivalence ==> eq ==> iffT) (@Proper A).
+Proof.
+  intros A R R' HRR' x y <-. red in HRR'.
+  split ; red ; intros. 
+  now apply (fst (HRR' _ _)). 
+  now apply (snd (HRR' _ _)).
+Qed.
+
+Ltac proper_reflexive :=
+  match goal with
+    | [ _ : normalization_done |- _ ] => fail 1
+    | _ => class_apply proper_eq || class_apply @reflexive_proper
+  end.
+
+
+Hint Extern 1 (subrelation (flip _) _) => class_apply @flip1 : typeclass_instances.
+Hint Extern 1 (subrelation _ (flip _)) => class_apply @flip2 : typeclass_instances.
+
+Hint Extern 1 (Proper _ (complement _)) => apply @complement_proper 
+  : typeclass_instances.
+Hint Extern 1 (Proper _ (flip _)) => apply @flip_proper 
+  : typeclass_instances.
+Hint Extern 2 (@Proper _ (flip _) _) => class_apply @proper_flip_proper 
+  : typeclass_instances.
+Hint Extern 4 (@Proper _ _ _) => partial_application_tactic 
+  : typeclass_instances.
+Hint Extern 7 (@Proper _ _ _) => proper_reflexive 
+  : typeclass_instances.
+
+(** Special-purpose class to do normalization of signatures w.r.t. flip. *)
+
+Section Normalize.
+  Context (A : Type).
+
+  Class Normalizes (m : crelation A) (m' : crelation A) : Prop :=
+    normalizes : relation_equivalence m m'.
+  
+  (** Current strategy: add [flip] everywhere and reduce using [subrelation]
+   afterwards. *)
+
+  Lemma proper_normalizes_proper `(Normalizes R0 R1, Proper A R1 m) : Proper R0 m.
+  Proof.
+    red in H, H0. red in H.
+    apply (snd (H _ _)). 
+    assumption.
+  Qed.
+
+  Lemma flip_atom R : Normalizes R (flip (flip R)).
+  Proof.
+    firstorder.
+  Qed.
+
+End Normalize.
+
+Lemma flip_arrow `(NA : Normalizes A R (flip R'''), NB : Normalizes B R' (flip R'')) :
+  Normalizes (A -> B) (R ==> R') (flip (R''' ==> R'')%signature).
+Proof. 
+  unfold Normalizes in *. intros.
+  rewrite NA, NB. firstorder. 
+Qed.
+
+Ltac normalizes :=
+  match goal with
+    | [ |- Normalizes _ (respectful _ _) _ ] => class_apply @flip_arrow
+    | _ => class_apply @flip_atom
+  end.
+
+Ltac proper_normalization :=
+  match goal with
+    | [ _ : normalization_done |- _ ] => fail 1
+    | [ _ : apply_subrelation |- @Proper _ ?R _ ] => 
+      let H := fresh "H" in
+      set(H:=did_normalization) ; class_apply @proper_normalizes_proper
+  end.
+
+Hint Extern 1 (Normalizes _ _ _) => normalizes : typeclass_instances.
+Hint Extern 6 (@Proper _ _ _) => proper_normalization 
+  : typeclass_instances.
+
+(** When the crelation on the domain is symmetric, we can
+    flip the crelation on the codomain. Same for binary functions. *)
+
+Lemma proper_sym_flip :
+ forall `(Symmetric A R1)`(Proper (A->B) (R1==>R2) f),
+ Proper (R1==>flip 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==>flip 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 crelation on the domain is symmetric, a predicate is
+  compatible with [iff] as soon as it is compatible with [impl].
+  Same with a binary crelation. *)
+
+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_arrow_iffT : forall `(Symmetric A R)`(Proper _ (R==>arrow) f),
+ Proper (R==>iffT) 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.
+
+Lemma proper_sym_arrow_iffT_2 :
+ forall `(Symmetric A R)`(Symmetric B R')`(Proper _ (R==>R'==>arrow) f),
+ Proper (R==>R'==>iffT) 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. *)
+Require Import Relation_Definitions.
+
+Instance PartialOrder_proper_type `(PartialOrder A eqA R) :
+  Proper (eqA==>eqA==>iffT) R.
+Proof.
+intros.
+apply proper_sym_arrow_iffT_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.
+
+(** 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==>iffT) 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==>iffT) 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 (StrictOrder (relation_conjunction _ _)) => 
+  class_apply PartialOrder_StrictOrder : typeclass_instances.
+
+Hint Extern 4 (PartialOrder _ (relation_disjunction _ _)) => 
+  class_apply StrictOrder_PartialOrder : typeclass_instances.
diff --git a/theories/Classes/CRelationClasses.v b/theories/Classes/CRelationClasses.v
new file mode 100644
index 00000000..35b2b8a3
--- /dev/null
+++ b/theories/Classes/CRelationClasses.v
@@ -0,0 +1,359 @@
+(* -*- coding: utf-8 -*- *)
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(** * 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 - University Paris Sud
+*)
+
+Require Export Coq.Classes.Init.
+Require Import Coq.Program.Basics.
+Require Import Coq.Program.Tactics.
+
+Generalizable Variables A B C D R S T U l eqA eqB eqC eqD.
+
+Set Universe Polymorphism.
+
+Definition crelation (A : Type) := A -> A -> Type.
+
+Definition arrow (A B : Type) := A -> B.
+
+Definition flip {A B C : Type} (f : A -> B -> C) := fun x y => f y x.
+
+Definition iffT (A B : Type) := ((A -> B) * (B -> A))%type.
+
+(** We allow to unfold the [crelation] definition while doing morphism search. *)
+
+Section Defs.
+  Context {A : Type}.
+
+  (** We rebind crelational properties in separate classes to be able to overload each proof. *)
+
+  Class Reflexive (R : crelation A) :=
+    reflexivity : forall x : A, R x x.
+
+  Definition complement (R : crelation A) : crelation A := 
+    fun x y => R x y -> False.
+
+  (** Opaque for proof-search. *)
+  Typeclasses Opaque complement iffT.
+  
+  (** These are convertible. *)
+  Lemma complement_inverse R : complement (flip R) = flip (complement R).
+  Proof. reflexivity. Qed.
+
+  Class Irreflexive (R : crelation A) :=
+    irreflexivity : Reflexive (complement R).
+
+  Class Symmetric (R : crelation A) :=
+    symmetry : forall {x y}, R x y -> R y x.
+  
+  Class Asymmetric (R : crelation A) :=
+    asymmetry : forall {x y}, R x y -> (complement R y x : Type).
+  
+  Class Transitive (R : crelation A) :=
+    transitivity : forall {x y z}, R x y -> R y z -> R x z.
+
+  (** Various combinations of reflexivity, symmetry and transitivity. *)
+  
+  (** A [PreOrder] is both Reflexive and Transitive. *)
+
+  Class PreOrder (R : crelation A)  := {
+    PreOrder_Reflexive :> Reflexive R | 2 ;
+    PreOrder_Transitive :> Transitive R | 2 }.
+
+  (** A [StrictOrder] is both Irreflexive and Transitive. *)
+
+  Class StrictOrder (R : crelation A)  := {
+    StrictOrder_Irreflexive :> Irreflexive R ;
+    StrictOrder_Transitive :> Transitive R }.
+
+  (** By definition, a strict order is also asymmetric *)
+  Global Instance StrictOrder_Asymmetric `(StrictOrder R) : Asymmetric R.
+  Proof. firstorder. Qed.
+
+  (** A partial equivalence crelation is Symmetric and Transitive. *)
+  
+  Class PER (R : crelation A)  := {
+    PER_Symmetric :> Symmetric R | 3 ;
+    PER_Transitive :> Transitive R | 3 }.
+
+  (** Equivalence crelations. *)
+
+  Class Equivalence (R : crelation A)  := {
+    Equivalence_Reflexive :> Reflexive R ;
+    Equivalence_Symmetric :> Symmetric R ;
+    Equivalence_Transitive :> Transitive R }.
+
+  (** An Equivalence is a PER plus reflexivity. *)
+  
+  Global Instance Equivalence_PER {R} `(Equivalence R) : PER R | 10 :=
+    { PER_Symmetric := Equivalence_Symmetric ;
+      PER_Transitive := Equivalence_Transitive }.
+
+  (** We can now define antisymmetry w.r.t. an equivalence crelation on the carrier. *)
+  
+  Class Antisymmetric eqA `{equ : Equivalence eqA} (R : crelation A) :=
+    antisymmetry : forall {x y}, R x y -> R y x -> eqA x y.
+
+  Class subrelation (R R' : crelation A) :=
+    is_subrelation : forall {x y}, R x y -> R' x y.
+  
+  (** Any symmetric crelation is equal to its inverse. *)
+  
+  Lemma subrelation_symmetric R `(Symmetric R) : subrelation (flip R) R.
+  Proof. hnf. intros x y H'. red in H'. apply symmetry. assumption. Qed.
+
+  Section flip.
+  
+    Lemma flip_Reflexive `{Reflexive R} : Reflexive (flip R).
+    Proof. tauto. Qed.
+    
+    Program Definition flip_Irreflexive `(Irreflexive R) : Irreflexive (flip R) :=
+      irreflexivity (R:=R).
+    
+    Program Definition flip_Symmetric `(Symmetric R) : Symmetric (flip R) :=
+      fun x y H => symmetry (R:=R) H.
+    
+    Program Definition flip_Asymmetric `(Asymmetric R) : Asymmetric (flip R) :=
+      fun x y H H' => asymmetry (R:=R) H H'.
+    
+    Program Definition flip_Transitive `(Transitive R) : Transitive (flip R) :=
+      fun x y z H H' => transitivity (R:=R) H' H.
+
+    Program Definition flip_Antisymmetric `(Antisymmetric eqA R) :
+      Antisymmetric eqA (flip R).
+    Proof. firstorder. Qed.
+
+    (** Inversing the larger structures *)
+
+    Lemma flip_PreOrder `(PreOrder R) : PreOrder (flip R).
+    Proof. firstorder. Qed.
+
+    Lemma flip_StrictOrder `(StrictOrder R) : StrictOrder (flip R).
+    Proof. firstorder. Qed.
+
+    Lemma flip_PER `(PER R) : PER (flip R).
+    Proof. firstorder. Qed.
+
+    Lemma flip_Equivalence `(Equivalence R) : Equivalence (flip R).
+    Proof. firstorder. Qed.
+
+  End flip.
+
+  Section complement.
+
+    Definition complement_Irreflexive `(Reflexive R)
+      : Irreflexive (complement R).
+    Proof. firstorder. Qed.
+
+    Definition complement_Symmetric `(Symmetric R) : Symmetric (complement R).
+    Proof. firstorder. Qed.
+  End complement.
+
+
+  (** Rewrite crelation on a given support: declares a crelation as a rewrite
+   crelation 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
+   crelations. This is also done automatically by the [Declare Relation A RA]
+   commands. *)
+
+  Class RewriteRelation (RA : crelation A).
+
+  (** Any [Equivalence] declared in the context is automatically considered
+   a rewrite crelation. *)
+    
+  Global Instance equivalence_rewrite_crelation `(Equivalence eqA) : RewriteRelation eqA.
+
+  (** Leibniz equality. *)
+  Section Leibniz.
+    Global Instance eq_Reflexive : Reflexive (@eq A) := @eq_refl A.
+    Global Instance eq_Symmetric : Symmetric (@eq A) := @eq_sym A.
+    Global Instance eq_Transitive : Transitive (@eq A) := @eq_trans A.
+    
+    (** Leibinz equality [eq] is an equivalence crelation.
+        The instance has low priority as it is always applicable
+        if only the type is constrained. *)
+    
+    Global Program Instance eq_equivalence : Equivalence (@eq A) | 10.
+  End Leibniz.
+  
+End Defs.
+
+(** Default rewrite crelations handled by [setoid_rewrite]. *)
+Instance: RewriteRelation impl.
+Instance: RewriteRelation iff.
+
+(** Hints to drive the typeclass resolution avoiding loops
+ due to the use of full unification. *)
+Hint Extern 1 (Reflexive (complement _)) => class_apply @irreflexivity : typeclass_instances.
+Hint Extern 3 (Symmetric (complement _)) => class_apply complement_Symmetric : typeclass_instances.
+Hint Extern 3 (Irreflexive (complement _)) => class_apply complement_Irreflexive : typeclass_instances.
+
+Hint Extern 3 (Reflexive (flip _)) => apply flip_Reflexive : typeclass_instances.
+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 (Antisymmetric (flip _)) => class_apply flip_Antisymmetric : typeclass_instances.
+Hint Extern 3 (Transitive (flip _)) => class_apply flip_Transitive : typeclass_instances.
+Hint Extern 3 (StrictOrder (flip _)) => class_apply flip_StrictOrder : typeclass_instances.
+Hint Extern 3 (PreOrder (flip _)) => class_apply flip_PreOrder : typeclass_instances.
+
+Hint Extern 4 (subrelation (flip _) _) => 
+  class_apply @subrelation_symmetric : typeclass_instances.
+
+Hint Resolve irreflexivity : ord.
+
+Unset Implicit Arguments.
+
+(** A HintDb for crelations. *)
+
+Ltac solve_crelation :=
+  match goal with
+  | [ |- ?R ?x ?x ] => reflexivity
+  | [ H : ?R ?x ?y |- ?R ?y ?x ] => symmetry ; exact H
+  end.
+
+Hint Extern 4 => solve_crelation : crelations.
+
+(** We can already dualize all these properties. *)
+
+(** * 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) :=
+  first [ refine t | refine (t _) | refine (t _ _) | refine (t _ _ _) | refine (t _ _ _ _) |
+    refine (t _ _ _ _ _) | refine (t _ _ _ _ _ _) | refine (t _ _ _ _ _ _ _) ].
+
+Ltac simpl_crelation :=
+  unfold flip, impl, arrow ; try reduce ; program_simpl ;
+    try ( solve [ dintuition ]).
+
+Local Obligation Tactic := simpl_crelation.
+
+(** Logical implication. *)
+
+Program Instance impl_Reflexive : Reflexive impl.
+Program Instance impl_Transitive : Transitive impl.
+
+(** Logical equivalence. *)
+
+Instance iff_Reflexive : Reflexive iff := iff_refl.
+Instance iff_Symmetric : Symmetric iff := iff_sym.
+Instance iff_Transitive : Transitive iff := iff_trans.
+
+(** Logical equivalence [iff] is an equivalence crelation. *)
+
+Program Instance iff_equivalence : Equivalence iff. 
+Program Instance arrow_Reflexive : Reflexive arrow.
+Program Instance arrow_Transitive : Transitive arrow.
+
+Instance iffT_Reflexive : Reflexive iffT. 
+Proof. firstorder. Defined.
+Instance iffT_Symmetric : Symmetric iffT. 
+Proof. firstorder. Defined. 
+Instance iffT_Transitive : Transitive iffT.
+Proof. firstorder. Defined.
+
+(** We now develop a generalization of results on crelations for arbitrary predicates.
+   The resulting theory can be applied to homogeneous binary crelations but also to
+   arbitrary n-ary predicates. *)
+
+Local Open Scope list_scope.
+
+(** A compact representation of non-dependent arities, with the codomain singled-out. *)
+
+(** We define the various operations which define the algebra on binary crelations *)
+Section Binary.
+  Context {A : Type}.
+
+  Definition relation_equivalence : crelation (crelation A) :=
+    fun R R' => forall x y, iffT (R x y) (R' x y).
+
+  Global Instance: RewriteRelation relation_equivalence.
+  
+  Definition relation_conjunction (R : crelation A) (R' : crelation A) : crelation A :=
+    fun x y => prod (R x y) (R' x y).
+
+  Definition relation_disjunction (R : crelation A) (R' : crelation A) : crelation A :=
+    fun x y => sum (R x y) (R' x y).
+  
+  (** Relation equivalence is an equivalence, and subrelation defines a partial order. *)
+  
+  Set Automatic Introduction.
+  
+  Global Instance relation_equivalence_equivalence :
+    Equivalence relation_equivalence.
+  Proof. split; red; unfold relation_equivalence, iffT. firstorder. 
+    firstorder. 
+    intros. specialize (X x0 y0). specialize (X0 x0 y0). firstorder.
+  Qed.
+    
+  Global Instance relation_implication_preorder : PreOrder (@subrelation A).
+  Proof. firstorder. Qed.
+
+  (** *** Partial Order.
+   A partial order is a preorder which is additionally antisymmetric.
+   We give an equivalent definition, up-to an equivalence crelation
+   on the carrier. *)
+
+  Class PartialOrder eqA `{equ : Equivalence A eqA} R `{preo : PreOrder A R} :=
+    partial_order_equivalence : relation_equivalence eqA (relation_conjunction R (flip R)).
+  
+  (** 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] *)
+
+  Global Instance partial_order_antisym `(PartialOrder eqA R) : ! Antisymmetric A eqA R.
+  Proof with auto.
+    reduce_goal.
+    apply H. firstorder.
+  Qed.
+
+  Lemma PartialOrder_inverse `(PartialOrder eqA R) : PartialOrder eqA (flip R).
+  Proof. unfold flip; constructor; unfold flip. intros. apply H. apply symmetry. apply X.
+         unfold relation_conjunction. intros [H1 H2]. apply H. constructor; assumption. Qed.
+End Binary.
+
+Hint Extern 3 (PartialOrder (flip _)) => class_apply PartialOrder_inverse : typeclass_instances.
+
+(** The partial order defined by subrelation and crelation equivalence. *)
+
+(* Program Instance subrelation_partial_order : *)
+(*   ! PartialOrder (crelation A) relation_equivalence subrelation. *)
+(* Obligation Tactic := idtac. *)
+
+(* Next Obligation. *)
+(* Proof. *)
+(*   intros x. refine (fun x => x). *)
+(* Qed. *)
+
+Typeclasses Opaque relation_equivalence.
+
+
diff --git a/theories/Classes/DecidableClass.v b/theories/Classes/DecidableClass.v
new file mode 100644
index 00000000..9fe3d0fe
--- /dev/null
+++ b/theories/Classes/DecidableClass.v
@@ -0,0 +1,92 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(** * A typeclass to ease the handling of decidable properties. *)
+
+(** A proposition is decidable whenever it is reflected by a boolean. *)
+
+Class Decidable (P : Prop) := {
+  Decidable_witness : bool;
+  Decidable_spec : Decidable_witness = true <-> P
+}.
+
+(** Alternative ways of specifying the reflection property. *)
+
+Lemma Decidable_sound : forall P (H : Decidable P),
+  Decidable_witness = true -> P.
+Proof.
+intros P H Hp; apply -> Decidable_spec; assumption.
+Qed.
+
+Lemma Decidable_complete : forall P (H : Decidable P),
+  P -> Decidable_witness = true.
+Proof.
+intros P H Hp; apply <- Decidable_spec; assumption.
+Qed.
+
+Lemma Decidable_sound_alt : forall P (H : Decidable P),
+   ~ P -> Decidable_witness = false.
+Proof.
+intros P [wit spec] Hd; simpl; destruct wit; tauto.
+Qed.
+
+Lemma Decidable_complete_alt : forall P (H : Decidable P),
+  Decidable_witness = false -> ~ P.
+Proof.
+intros P [wit spec] Hd Hc; simpl in *; intuition congruence.
+Qed.
+
+(** The generic function that should be used to program, together with some
+  useful tactics. *)
+
+Definition decide P {H : Decidable P} := Decidable_witness (Decidable:=H).
+
+Ltac _decide_ P H :=
+  let b := fresh "b" in
+  set (b := decide P) in *;
+  assert (H : decide P = b) by reflexivity;
+  clearbody b;
+  destruct b; [apply Decidable_sound in H|apply Decidable_complete_alt in H].
+
+Tactic Notation "decide" constr(P) "as" ident(H) :=
+  _decide_ P H.
+
+Tactic Notation "decide" constr(P) :=
+  let H := fresh "H" in _decide_ P H.
+
+(** Some usual instances. *)
+
+Require Import Bool Arith ZArith.
+
+Program Instance Decidable_eq_bool : forall (x y : bool), Decidable (eq x y) := {
+  Decidable_witness := Bool.eqb x y
+}.
+Next Obligation.
+ apply eqb_true_iff.
+Qed.
+
+Program Instance Decidable_eq_nat : forall (x y : nat), Decidable (eq x y) := {
+  Decidable_witness := Nat.eqb x y
+}.
+Next Obligation.
+ apply Nat.eqb_eq.
+Qed.
+
+Program Instance Decidable_le_nat : forall (x y : nat), Decidable (x <= y) := {
+  Decidable_witness := Nat.leb x y
+}.
+Next Obligation.
+ apply Nat.leb_le.
+Qed.
+
+Program Instance Decidable_eq_Z : forall (x y : Z), Decidable (eq x y) := {
+  Decidable_witness := Z.eqb x y
+}.
+Next Obligation.
+ apply Z.eqb_eq.
+Qed.
diff --git a/theories/Classes/EquivDec.v b/theories/Classes/EquivDec.v
index 8e3715ff..59e800c2 100644
--- a/theories/Classes/EquivDec.v
+++ b/theories/Classes/EquivDec.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -53,7 +53,9 @@ Local Open Scope program_scope.
 
 (** Invert the branches. *)
 
-Program Definition nequiv_dec `{EqDec A} (x y : A) : { x =/= y } + { x === y } := swap_sumbool (x == y).
+Program Definition nequiv_dec `{EqDec A} (x y : A) : { x =/= y } + { x === y } := 
+          swap_sumbool (x == y).
+
 
 (** Overloaded notation for inequality. *)
 
@@ -138,8 +140,7 @@ Program Instance list_eqdec `(eqa : EqDec A eq) : ! EqDec (list A) eq :=
       | _, _ => in_right
     end }.
 
-  Solve Obligations using unfold equiv, complement in * ; program_simpl ; intuition (discriminate || eauto).
-
-  Next Obligation. destruct y ; intuition eauto. Defined.
+  Next Obligation. destruct y ; unfold not in *; eauto. Defined.
 
-  Solve Obligations using unfold equiv, complement in * ; program_simpl ; intuition (discriminate || eauto).
+  Solve Obligations with unfold equiv, complement in * ; 
+    program_simpl ; intuition (discriminate || eauto).
diff --git a/theories/Classes/Equivalence.v b/theories/Classes/Equivalence.v
index 0e9adf64..c281af80 100644
--- a/theories/Classes/Equivalence.v
+++ b/theories/Classes/Equivalence.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -24,7 +24,7 @@ Set Implicit Arguments.
 Unset Strict Implicit.
 
 Generalizable Variables A R eqA B S eqB.
-Local Obligation Tactic := simpl_relation.
+Local Obligation Tactic := try solve [simpl_relation].
 
 Local Open Scope signature_scope.
 
@@ -56,8 +56,8 @@ Program Instance equiv_symmetric `(sa : Equivalence A) : Symmetric equiv.
 Program Instance equiv_transitive `(sa : Equivalence A) : Transitive equiv.
 
   Next Obligation.
-  Proof.
-    transitivity y ; auto.
+  Proof. intros A R sa x y z Hxy Hyz.
+         now transitivity y.
   Qed.
 
 (** Use the [substitute] command which substitutes an equivalence in every hypothesis. *)
@@ -105,27 +105,35 @@ Section Respecting.
   (** 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)).
+    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.
+  Solve Obligations with unfold respecting in * ; simpl_relation ; program_simpl.
 
   Next Obligation.
-  Proof.
-    unfold respecting in *. program_simpl. transitivity (y y0); auto. apply H0. reflexivity.
+  Proof. 
+    intros. intros f g h H H' x y Rxy.
+    unfold respecting in *. program_simpl. transitivity (g y); auto. firstorder.
   Qed.
 
 End Respecting.
 
 (** The default equivalence on function spaces, with higher-priority than [eq]. *)
 
-Program Instance pointwise_equivalence {A} `(eqb : Equivalence B eqB) :
+Instance pointwise_reflexive {A} `(reflb : Reflexive B eqB) :
+  Reflexive (pointwise_relation A eqB) | 9.
+Proof. firstorder. Qed.
+Instance pointwise_symmetric {A} `(symb : Symmetric B eqB) :
+  Symmetric (pointwise_relation A eqB) | 9.
+Proof. firstorder. Qed.
+Instance pointwise_transitive {A} `(transb : Transitive B eqB) :
+  Transitive (pointwise_relation A eqB) | 9.
+Proof. firstorder. Qed.
+Instance pointwise_equivalence {A} `(eqb : Equivalence B eqB) :
   Equivalence (pointwise_relation A eqB) | 9.
-
-  Next Obligation.
-  Proof.
-    transitivity (y a) ; auto.
-  Qed.
+Proof. split; apply _. Qed.
diff --git a/theories/Classes/Init.v b/theories/Classes/Init.v
index 1a56c1a3..9574cf85 100644
--- a/theories/Classes/Init.v
+++ b/theories/Classes/Init.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/theories/Classes/Morphisms.v b/theories/Classes/Morphisms.v
index 9d5a3233..1bdce654 100644
--- a/theories/Classes/Morphisms.v
+++ b/theories/Classes/Morphisms.v
@@ -1,7 +1,7 @@
 (* -*- coding: utf-8 -*- *)
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -18,7 +18,7 @@ Require Import Coq.Program.Tactics.
 Require Import Coq.Relations.Relation_Definitions.
 Require Export Coq.Classes.RelationClasses.
 
-Generalizable All Variables.
+Generalizable Variables A eqA B C D R RA RB RC m f x y.
 Local Obligation Tactic := simpl_relation.
 
 (** * Morphisms.
@@ -29,15 +29,39 @@ Local Obligation Tactic := simpl_relation.
 (** 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 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
+Section Proper.
+  Let U := Type.
+  Context {A B : U}.
+
+  Class Proper (R : relation A) (m : A) : Prop :=
+    proper_prf : R m m.
+
+  (** 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 [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. *)
+
+  Class ProperProxy (R : relation A) (m : A) : Prop :=
+    proper_proxy : R m m.
+
+  Lemma eq_proper_proxy (x : A) : ProperProxy (@eq A) x.
+  Proof. firstorder. Qed.
+  
+  Lemma reflexive_proper_proxy `(Reflexive A R) (x : A) : ProperProxy R x.
+  Proof. firstorder. Qed.
+
+  Lemma proper_proper_proxy x `(Proper R x) : ProperProxy R x.
+  Proof. firstorder. Qed.
+
+  (** 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)
@@ -45,18 +69,24 @@ Definition respectful_hetero
     (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. *)
+  (** The non-dependent version is an instance where we forget dependencies. *)
+  
+  Definition respectful (R : relation A) (R' : relation B) : relation (A -> B) :=
+    Eval compute in @respectful_hetero A A (fun _ => B) (fun _ => B) R (fun _ _ => R').
 
-Definition respectful {A B : Type}
-  (R : relation A) (R' : relation B) : relation (A -> B) :=
-  Eval compute in @respectful_hetero A A (fun _ => B) (fun _ => B) R (fun _ _ => R').
+End Proper.
 
-(** Notations reminiscent of the old syntax for declaring morphisms. *)
+(** We favor the use of Leibniz equality or a declared reflexive relation 
+  when resolving [ProperProxy], otherwise, if the relation is given (not an evar),
+  we fall back to [Proper]. *)
+Hint Extern 1 (ProperProxy _ _) => 
+  class_apply @eq_proper_proxy || class_apply @reflexive_proper_proxy : typeclass_instances.
 
-Delimit Scope signature_scope with signature.
+Hint Extern 2 (ProperProxy ?R _) => 
+  not_evar R; class_apply @proper_proper_proxy : typeclass_instances.
 
-Arguments Proper {A}%type R%signature m.
-Arguments respectful {A B}%type (R R')%signature _ _.
+(** Notations reminiscent of the old syntax for declaring morphisms. *)
+Delimit Scope signature_scope with signature.
 
 Module ProperNotations.
 
@@ -66,11 +96,14 @@ Module ProperNotations.
   Notation " R ==> R' " := (@respectful _ _ (R%signature) (R'%signature))
     (right associativity, at level 55) : signature_scope.
 
-  Notation " R --> R' " := (@respectful _ _ (inverse (R%signature)) (R'%signature))
+  Notation " R --> R' " := (@respectful _ _ (flip (R%signature)) (R'%signature))
     (right associativity, at level 55) : signature_scope.
 
 End ProperNotations.
 
+Arguments Proper {A}%type R%signature m.
+Arguments respectful {A B}%type (R R')%signature _ _.
+
 Export ProperNotations.
 
 Local Open Scope signature_scope.
@@ -106,80 +139,89 @@ Ltac f_equiv :=
     assert (H : (Rx==>R)%signature f f');
     unfold Rx in *; clear Rx; [ f_equiv | apply H; clear H; try reflexivity ]
   | |- ?R ?f ?f' =>
-    try reflexivity;
-    change (Proper R f); eauto with typeclass_instances; fail
+    solve [change (Proper R f); eauto with typeclass_instances | reflexivity ]
   | _ => idtac
  end.
 
-(** [forall_def] reifies the dependent product as a definition. *)
-
-Definition forall_def {A : Type} (B : A -> Type) : Type := forall x : A, B x.
-
-(** Dependent pointwise lifting of a relation on the range. *)
-
-Definition forall_relation {A : Type} {B : A -> Type}
- (sig : forall a, relation (B a)) : relation (forall x, B x) :=
- fun f g => forall a, sig a (f a) (g a).
-
-Arguments forall_relation {A B}%type sig%signature _ _.
-
-(** Non-dependent pointwise lifting *)
+Section Relations.
+  Let U := Type.
+  Context {A B : U} (P : A -> U).
+
+  (** [forall_def] reifies the dependent product as a definition. *)
+  
+  Definition forall_def : Type := forall x : A, P x.
+  
+  (** Dependent pointwise lifting of a relation on the range. *)
+  
+  Definition forall_relation 
+             (sig : forall a, relation (P a)) : relation (forall x, P x) :=
+    fun f g => forall a, sig a (f a) (g a).
+
+  (** Non-dependent pointwise lifting *)
+  Definition pointwise_relation (R : relation B) : relation (A -> B) :=
+    fun f g => forall a, R (f a) (g a).
+
+  Lemma pointwise_pointwise (R : relation B) :
+    relation_equivalence (pointwise_relation R) (@eq A ==> R).
+  Proof. intros. split; reduce; subst; firstorder. Qed.
+  
+  (** Subrelations induce a morphism on the identity. *)
+  
+  Global Instance subrelation_id_proper `(subrelation A RA RA') : Proper (RA ==> RA') id.
+  Proof. firstorder. Qed.
+
+  (** The subrelation property goes through products as usual. *)
+  
+  Lemma subrelation_respectful `(subl : subrelation A RA' RA, subr : subrelation B RB RB') :
+    subrelation (RA ==> RB) (RA' ==> RB').
+  Proof. unfold subrelation in *; firstorder. Qed.
+
+  (** And of course it is reflexive. *)
+  
+  Lemma subrelation_refl R : @subrelation A R R.
+  Proof. unfold subrelation; firstorder. Qed.
+
+  (** [Proper] is itself a covariant morphism for [subrelation].
+   We use an unconvertible premise to avoid looping.
+   *)
+  
+  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.
 
-Definition pointwise_relation (A : Type) {B : Type} (R : relation B) : relation (A -> B) :=
-  Eval compute in forall_relation (B:=fun _ => B) (fun _ => R).
+  Global Instance proper_subrelation_proper :
+    Proper (subrelation ++> eq ==> impl) (@Proper A).
+  Proof. reduce. subst. firstorder. Qed.
 
-Lemma pointwise_pointwise A B (R : relation B) :
-  relation_equivalence (pointwise_relation A R) (@eq A ==> R).
-Proof. intros. split. simpl_relation. firstorder. Qed.
-
-(** We can build a PER on the Coq function space if we have PERs on the domain and
-   codomain. *)
+  Global Instance pointwise_subrelation `(sub : subrelation B R R') :
+    subrelation (pointwise_relation R) (pointwise_relation R') | 4.
+  Proof. reduce. unfold pointwise_relation in *. apply sub. apply H. Qed.
+  
+  (** For dependent function types. *)
+  Lemma forall_subrelation (R S : forall x : A, relation (P x)) :
+    (forall a, subrelation (R a) (S a)) -> subrelation (forall_relation R) (forall_relation S).
+  Proof. reduce. apply H. apply H0. Qed.
+End Relations.
 
+Typeclasses Opaque respectful pointwise_relation forall_relation.
+Arguments forall_relation {A P}%type sig%signature _ _.
+Arguments pointwise_relation A%type {B}%type R%signature _ _.
+  
 Hint Unfold Reflexive : core.
 Hint Unfold Symmetric : core.
 Hint Unfold Transitive : core.
 
-Typeclasses Opaque respectful pointwise_relation forall_relation.
-
-Program Instance respectful_per `(PER A R, PER B R') : PER (R ==> R').
-
-  Next Obligation.
-  Proof with auto.
-    assert(R x0 x0).
-    transitivity y0... symmetry...
-    transitivity (y x0)...
-  Qed.
-
-(** Subrelations induce a morphism on the identity. *)
-
-Instance subrelation_id_proper `(subrelation A R₁ R₂) : Proper (R₁ ==> R₂) id.
-Proof. firstorder. Qed.
-
-(** The subrelation property goes through products as usual. *)
-
-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. *)
-
-Lemma subrelation_refl A R : @subrelation A R R.
-Proof. simpl_relation. Qed.
-
+(** Resolution with subrelation: favor decomposing products over applying reflexivity
+  for unconstrained goals. *)
 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.
 
-(** [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.
-
 CoInductive apply_subrelation : Prop := do_subrelation.
 
 Ltac proper_subrelation :=
@@ -189,117 +231,112 @@ Ltac proper_subrelation :=
 
 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]. *)
 
 Instance iff_impl_subrelation : subrelation iff impl | 2.
 Proof. firstorder. Qed.
 
-Instance iff_inverse_impl_subrelation : subrelation iff (inverse impl) | 2.
+Instance iff_flip_impl_subrelation : subrelation iff (flip impl) | 2.
 Proof. firstorder. Qed.
 
-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.
-
-(** 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.
+Section GenericInstances.
+  (* Share universes *)
+  Let U := Type.
+  Context {A B C : U}.
 
-Hint Extern 4 (subrelation (inverse _) _) => 
-  class_apply @subrelation_symmetric : typeclass_instances.
-
-(** The complement of a relation conserves its proper elements. *)
+  (** We can build a PER on the Coq function space if we have PERs on the domain and
+   codomain. *)
+  
+  Program Instance respectful_per `(PER A R, PER B R') : PER (R ==> R').
 
-Program Definition complement_proper
-  `(mR : Proper (A -> A -> Prop) (RA ==> RA ==> iff) R) :
-  Proper (RA ==> RA ==> iff) (complement R) := _.
+  Next Obligation.
+  Proof with auto.
+    assert(R x0 x0).
+    transitivity y0... symmetry...
+    transitivity (y x0)... 
+  Qed.
 
- Next Obligation.
+  (** The complement of a relation conserves its proper elements. *)
+  
+  Program Definition complement_proper
+          `(mR : Proper (A -> A -> Prop) (RA ==> RA ==> iff) R) :
+    Proper (RA ==> RA ==> iff) (complement R) := _.
+  
+  Next Obligation.
   Proof.
     unfold complement.
     pose (mR x y H x0 y0 H0).
     intuition.
   Qed.
  
-Hint Extern 1 (Proper _ (complement _)) => 
-  apply @complement_proper : typeclass_instances.
-
-(** The [inverse] too, actually the [flip] instance is a bit more general. *)
-
-Program Definition flip_proper
-  `(mor : Proper (A -> B -> C) (RA ==> RB ==> RC) f) :
-  Proper (RB ==> RA ==> RC) (flip f) := _.
+  (** The [flip] too, actually the [flip] instance is a bit more general. *)
 
+  Program Definition flip_proper
+          `(mor : Proper (A -> B -> C) (RA ==> RB ==> RC) f) :
+    Proper (RB ==> RA ==> RC) (flip f) := _.
+  
   Next Obligation.
   Proof.
     apply mor ; auto.
   Qed.
 
-Hint Extern 1 (Proper _ (flip _)) => 
-  apply @flip_proper : typeclass_instances.
 
-(** 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) : Proper (R --> R ++> impl) R.
-
+  
+  Global Program 
+  Instance trans_contra_co_morphism
+    `(Transitive A R) : Proper (R --> R ++> impl) R.
+  
   Next Obligation.
   Proof with auto.
     transitivity x...
     transitivity x0...
   Qed.
 
-(** Proper declarations for partial applications. *)
+  (** Proper declarations for partial applications. *)
 
-Program Instance trans_contra_inv_impl_morphism
-  `(Transitive A R) : Proper (R --> inverse impl) (R x) | 3.
+  Global Program 
+  Instance trans_contra_inv_impl_morphism
+  `(Transitive A R) : Proper (R --> flip impl) (R x) | 3.
 
   Next Obligation.
   Proof with auto.
     transitivity y...
   Qed.
 
-Program Instance trans_co_impl_morphism
-  `(Transitive A R) : Proper (R ++> impl) (R x) | 3.
+  Global Program 
+  Instance trans_co_impl_morphism
+    `(Transitive A R) : Proper (R ++> impl) (R x) | 3.
 
   Next Obligation.
   Proof with auto.
     transitivity x0...
   Qed.
 
-Program Instance trans_sym_co_inv_impl_morphism
-  `(PER A R) : Proper (R ++> inverse impl) (R x) | 3.
+  Global Program 
+  Instance trans_sym_co_inv_impl_morphism
+    `(PER A R) : Proper (R ++> flip impl) (R x) | 3.
 
   Next Obligation.
   Proof with auto.
     transitivity y... symmetry...
   Qed.
 
-Program Instance trans_sym_contra_impl_morphism
-  `(PER A R) : Proper (R --> impl) (R x) | 3.
+  Global Program Instance trans_sym_contra_impl_morphism
+    `(PER A R) : Proper (R --> impl) (R x) | 3.
 
   Next Obligation.
   Proof with auto.
     transitivity x0... symmetry...
   Qed.
 
-Program Instance per_partial_app_morphism
+  Global Program Instance per_partial_app_morphism
   `(PER A R) : Proper (R ==> iff) (R x) | 2.
 
   Next Obligation.
@@ -310,20 +347,21 @@ Program Instance per_partial_app_morphism
     symmetry...
   Qed.
 
-(** Every Transitive relation induces a morphism by "pushing" an [R x y] on the left of an [R x z] proof
-   to get an [R y z] goal. *)
+  (** Every Transitive relation induces a morphism by "pushing" an [R x y] on the left of an [R x z] proof to get an [R y z] goal. *)
 
-Program Instance trans_co_eq_inv_impl_morphism
-  `(Transitive A R) : Proper (R ==> (@eq A) ==> inverse impl) R | 2.
+  Global Program 
+  Instance trans_co_eq_inv_impl_morphism
+  `(Transitive A R) : Proper (R ==> (@eq A) ==> flip impl) R | 2.
 
   Next Obligation.
   Proof with auto.
     transitivity y...
   Qed.
 
-(** Every Symmetric and Transitive relation gives rise to an equivariant morphism. *)
+  (** Every Symmetric and Transitive relation gives rise to an equivariant morphism. *)
 
-Program Instance PER_morphism `(PER A R) : Proper (R ==> R ==> iff) R | 1.
+  Global Program 
+  Instance PER_morphism `(PER A R) : Proper (R ==> R ==> iff) R | 1.
 
   Next Obligation.
   Proof with auto.
@@ -333,11 +371,11 @@ Program Instance PER_morphism `(PER A R) : Proper (R ==> R ==> iff) R | 1.
     transitivity y... transitivity y0... symmetry...
   Qed.
 
-Lemma symmetric_equiv_inverse `(Symmetric A R) : relation_equivalence R (flip R).
-Proof. firstorder. Qed.
+  Lemma symmetric_equiv_flip `(Symmetric A R) : relation_equivalence R (flip R).
+  Proof. firstorder. Qed.
 
-Program Instance compose_proper A B C R₀ R₁ R₂ :
-  Proper ((R₁ ==> R₂) ==> (R₀ ==> R₁) ==> (R₀ ==> R₂)) (@compose A B C).
+  Global Program Instance compose_proper RA RB RC :
+    Proper ((RB ==> RC) ==> (RA ==> RB) ==> (RA ==> RC)) (@compose A B C).
 
   Next Obligation.
   Proof.
@@ -345,68 +383,84 @@ Program Instance compose_proper A B C R₀ R₁ R₂ :
     unfold compose. apply H. apply H0. apply H1.
   Qed.
 
-(** Coq functions are morphisms for Leibniz equality,
-   applied only if really needed. *)
-
-Instance reflexive_eq_dom_reflexive (A : Type) `(Reflexive B R') :
-  Reflexive (@Logic.eq A ==> R').
-Proof. simpl_relation. Qed.
+  (** Coq functions are morphisms for Leibniz equality,
+     applied only if really needed. *)
 
-(** [respectful] is a morphism for relation equivalence. *)
-
-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.
+  Global Instance reflexive_eq_dom_reflexive `(Reflexive B R') :
+    Reflexive (@Logic.eq A ==> R').
+  Proof. simpl_relation. Qed.
 
+  (** [respectful] is a morphism for relation equivalence. *)
+  
+  Global 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.
     assumption.
-
+    
     rewrite H0.
     apply H1.
     rewrite <- H.
     assumption.
-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
-   [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.*)
-
-Class ProperProxy {A} (R : relation A) (m : A) : Prop :=
-  proper_proxy : R m m.
-
-Lemma eq_proper_proxy A (x : A) : ProperProxy (@eq A) x.
-Proof. firstorder. Qed.
-
-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.
+  Qed.
 
-(** [R] is Reflexive, hence we can build the needed proof. *)
+  (** [R] is Reflexive, hence we can build the needed proof. *)
 
-Lemma Reflexive_partial_app_morphism `(Proper (A -> B) (R ==> R') m, ProperProxy A R x) :
-   Proper R' (m x).
-Proof. simpl_relation. Qed.
+  Lemma Reflexive_partial_app_morphism `(Proper (A -> B) (R ==> R') m, ProperProxy A R x) :
+    Proper R' (m x).
+  Proof. simpl_relation. Qed.
+  
+  Lemma flip_respectful (R : relation A) (R' : relation B) :
+    relation_equivalence (flip (R ==> R')) (flip R ==> flip R').
+  Proof.
+    intros.
+    unfold flip, respectful.
+    split ; intros ; intuition.
+  Qed.
 
-Class Params {A : Type} (of : A) (arity : nat).
+  
+  (** Treating flip: can't make them direct instances as we
+   need at least a [flip] present in the goal. *)
+  
+  Lemma flip1 `(subrelation A R' R) : subrelation (flip (flip R')) R.
+  Proof. firstorder. Qed.
+  
+  Lemma flip2 `(subrelation A R R') : subrelation R (flip (flip R')).
+  Proof. firstorder. Qed.
+  
+  (** That's if and only if *)
+  
+  Lemma eq_subrelation `(Reflexive A R) : subrelation (@eq A) R.
+  Proof. simpl_relation. Qed.
+
+  (** Once we have normalized, we will apply this instance to simplify the problem. *)
+  
+  Definition proper_flip_proper `(mor : Proper A R m) : Proper (flip R) m := mor.
+  
+  (** Every reflexive relation gives rise to a morphism, 
+  only for immediately solving goals without variables. *)
+  
+  Lemma reflexive_proper `{Reflexive A R} (x : A) : Proper R x.
+  Proof. firstorder. Qed.
+  
+  Lemma proper_eq (x : A) : Proper (@eq A) x.
+  Proof. intros. apply reflexive_proper. Qed.
+  
+End GenericInstances.
 
 Class PartialApplication.
 
 CoInductive normalization_done : Prop := did_normalization.
 
+Class Params {A : Type} (of : A) (arity : nat).
+
 Ltac partial_application_tactic :=
   let rec do_partial_apps H m cont := 
     match m with
@@ -450,68 +504,6 @@ Ltac partial_application_tactic :=
       end
   end.
 
-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').
-Proof.
-  intros.
-  unfold flip, respectful.
-  split ; intros ; intuition.
-Qed.
-
-(** Special-purpose class to do normalization of signatures w.r.t. inverse. *)
-
-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]
-   afterwards. *)
-
-Lemma inverse_atom A R : Normalizes A R (inverse (inverse R)).
-Proof.
-  firstorder.
-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 in *. intros. 
-  rewrite NA, NB. firstorder.
-Qed.
-
-Ltac inverse :=
-  match goal with
-    | [ |- 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
-   need at least a [flip] present in the goal. *)
-
-Lemma inverse1 `(subrelation A R' R) : subrelation (inverse (inverse R')) R.
-Proof. firstorder. Qed.
-
-Lemma inverse2 `(subrelation A R R') : subrelation R (inverse (inverse R')).
-Proof. firstorder. Qed.
-
-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 proper_inverse_proper `(mor : Proper A R m) : Proper (inverse R) m := mor.
-
-Hint Extern 2 (@Proper _ (flip _) _) => class_apply @proper_inverse_proper : typeclass_instances.
-
 (** Bootstrap !!! *)
 
 Instance proper_proper : Proper (relation_equivalence ==> eq ==> iff) (@Proper A).
@@ -525,46 +517,88 @@ Proof.
   apply H0.
 Qed.
 
-Lemma proper_normalizes_proper `(Normalizes A R0 R1, Proper A R1 m) : Proper R0 m.
-Proof.
-  red in H, H0.
-  setoid_rewrite H.
-  assumption.
-Qed.
-
-Ltac proper_normalization :=
+Ltac proper_reflexive :=
   match goal with
     | [ _ : normalization_done |- _ ] => fail 1
-    | [ _ : apply_subrelation |- @Proper _ ?R _ ] => let H := fresh "H" in
-      set(H:=did_normalization) ; class_apply @proper_normalizes_proper
+    | _ => class_apply proper_eq || class_apply @reflexive_proper
   end.
 
-Hint Extern 6 (@Proper _ _ _) => proper_normalization : typeclass_instances.
 
-(** Every reflexive relation gives rise to a morphism, only for immediately solving goals without variables. *)
+Hint Extern 1 (subrelation (flip _) _) => class_apply @flip1 : typeclass_instances.
+Hint Extern 1 (subrelation _ (flip _)) => class_apply @flip2 : typeclass_instances.
 
-Lemma reflexive_proper `{Reflexive A R} (x : A)
-   : Proper R x.
-Proof. firstorder. Qed.
+Hint Extern 1 (Proper _ (complement _)) => apply @complement_proper 
+  : typeclass_instances.
+Hint Extern 1 (Proper _ (flip _)) => apply @flip_proper 
+  : typeclass_instances.
+Hint Extern 2 (@Proper _ (flip _) _) => class_apply @proper_flip_proper 
+  : typeclass_instances.
+Hint Extern 4 (@Proper _ _ _) => partial_application_tactic 
+  : typeclass_instances.
+Hint Extern 7 (@Proper _ _ _) => proper_reflexive 
+  : typeclass_instances.
 
-Lemma proper_eq A (x : A) : Proper (@eq A) x.
-Proof. intros. apply reflexive_proper. Qed.
+(** Special-purpose class to do normalization of signatures w.r.t. flip. *)
 
-Ltac proper_reflexive :=
+Section Normalize.
+  Context (A : Type).
+
+  Class Normalizes (m : relation A) (m' : relation A) : Prop :=
+    normalizes : relation_equivalence m m'.
+  
+  (** Current strategy: add [flip] everywhere and reduce using [subrelation]
+   afterwards. *)
+
+  Lemma proper_normalizes_proper `(Normalizes R0 R1, Proper A R1 m) : Proper R0 m.
+  Proof.
+    red in H, H0.
+    rewrite H.
+    assumption.
+  Qed.
+
+  Lemma flip_atom R : Normalizes R (flip (flip R)).
+  Proof.
+    firstorder.
+  Qed.
+
+End Normalize.
+
+Lemma flip_arrow {A : Type} {B : Type}
+      `(NA : Normalizes A R (flip R'''), NB : Normalizes B R' (flip R'')) :
+  Normalizes (A -> B) (R ==> R') (flip (R''' ==> R'')%signature).
+Proof. 
+  unfold Normalizes in *. intros.
+  unfold relation_equivalence in *. 
+  unfold predicate_equivalence in *. simpl in *.
+  unfold respectful. unfold flip in *. firstorder.
+  apply NB. apply H. apply NA. apply H0.
+  apply NB. apply H. apply NA. apply H0.
+Qed.
+
+Ltac normalizes :=
   match goal with
-    | [ _ : normalization_done |- _ ] => fail 1
-    | _ => class_apply proper_eq || class_apply @reflexive_proper
+    | [ |- Normalizes _ (respectful _ _) _ ] => class_apply @flip_arrow
+    | _ => class_apply @flip_atom
   end.
 
-Hint Extern 7 (@Proper _ _ _) => proper_reflexive : typeclass_instances.
+Ltac proper_normalization :=
+  match goal with
+    | [ _ : normalization_done |- _ ] => fail 1
+    | [ _ : apply_subrelation |- @Proper _ ?R _ ] => 
+      let H := fresh "H" in
+      set(H:=did_normalization) ; class_apply @proper_normalizes_proper
+  end.
 
+Hint Extern 1 (Normalizes _ _ _) => normalizes : typeclass_instances.
+Hint Extern 6 (@Proper _ _ _) => proper_normalization 
+  : typeclass_instances.
 
 (** When the relation on the domain is symmetric, we can
-    inverse the relation on the codomain. Same for binary functions. *)
+    flip 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.
+ Proper (R1==>flip R2) f.
 Proof.
 intros A R1 Sym B R2 f Hf.
 intros x x' Hxx'. apply Hf, Sym, Hxx'.
@@ -572,7 +606,7 @@ 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.
+ Proper (R1==>R2==>flip R3) f.
 Proof.
 intros A R1 Sym1 B R2 Sym2 C R3 f Hf.
 intros x x' Hxx' y y' Hyy'. apply Hf; auto.
@@ -627,8 +661,6 @@ 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].
@@ -659,5 +691,8 @@ elim (StrictOrder_Irreflexive x).
 transitivity y; auto.
 Qed.
 
+Hint Extern 4 (StrictOrder (relation_conjunction _ _)) => 
+  class_apply PartialOrder_StrictOrder : typeclass_instances.
+
 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 c3737658..096c96e5 100644
--- a/theories/Classes/Morphisms_Prop.v
+++ b/theories/Classes/Morphisms_Prop.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -16,7 +16,7 @@ Require Import Coq.Classes.Morphisms.
 Require Import Coq.Program.Basics.
 Require Import Coq.Program.Tactics.
 
-Local Obligation Tactic := simpl_relation.
+Local Obligation Tactic := try solve [simpl_relation | firstorder auto].
 
 (** Standard instances for [not], [iff] and [impl]. *)
 
@@ -52,61 +52,20 @@ Program Instance iff_iff_iff_impl_morphism : Proper (iff ==> iff ==> iff) impl.
 
 Program Instance ex_iff_morphism {A : Type} : Proper (pointwise_relation A iff ==> iff) (@ex A).
 
-  Next Obligation.
-  Proof.
-    unfold pointwise_relation in H.
-    split ; intros.
-    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} :
   Proper (pointwise_relation A impl ==> impl) (@ex A) | 1.
 
-  Next Obligation.
-  Proof.
-    unfold pointwise_relation in H.
-    exists H0. apply H. assumption.
-  Qed.
-
-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.
-    exists H0. apply H. assumption.
-  Qed.
+Program Instance ex_flip_impl_morphism {A : Type} :
+  Proper (pointwise_relation A (flip impl) ==> flip impl) (@ex A) | 1.
 
 Program Instance all_iff_morphism {A : Type} :
   Proper (pointwise_relation A iff ==> iff) (@all A).
 
-  Next Obligation.
-  Proof.
-    unfold pointwise_relation, all in *.
-    intuition ; specialize (H x0) ; intuition.
-  Qed.
-
 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} :
-  Proper (pointwise_relation A (inverse impl) ==> inverse impl) (@all A) | 1.
-
-  Next Obligation.
-  Proof.
-    unfold pointwise_relation, all in *.
-    intuition ; specialize (H x0) ; intuition.
-  Qed.
+Program Instance all_flip_impl_morphism {A : Type} :
+  Proper (pointwise_relation A (flip impl) ==> flip impl) (@all A) | 1.
 
 (** Equivalent points are simultaneously accessible or not *)
 
@@ -116,13 +75,13 @@ Instance Acc_pt_morphism {A:Type}(E R : A->A->Prop)
 Proof.
  apply proper_sym_impl_iff; auto with *.
  intros x y EQ WF. apply Acc_intro; intros z Hz.
- rewrite <- EQ in Hz. now apply Acc_inv with x.
+rewrite <- EQ in Hz. now apply Acc_inv with x.
 Qed.
 
 (** Equivalent relations have the same accessible points *)
 
 Instance Acc_rel_morphism {A:Type} :
- Proper (@relation_equivalence A ==> Logic.eq ==> iff) (@Acc A).
+ Proper (relation_equivalence ==> Logic.eq ==> iff) (@Acc A).
 Proof.
  apply proper_sym_impl_iff_2. red; now symmetry. red; now symmetry.
  intros R R' EQ a a' Ha WF. subst a'.
@@ -133,7 +92,7 @@ Qed.
 (** Equivalent relations are simultaneously well-founded or not *)
 
 Instance well_founded_morphism {A : Type} :
- Proper (@relation_equivalence A ==> iff) (@well_founded A).
+ Proper (relation_equivalence ==> iff) (@well_founded A).
 Proof.
  unfold well_founded. solve_proper.
 Qed.
diff --git a/theories/Classes/Morphisms_Relations.v b/theories/Classes/Morphisms_Relations.v
index 34115e57..68a8c06a 100644
--- a/theories/Classes/Morphisms_Relations.v
+++ b/theories/Classes/Morphisms_Relations.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -30,8 +30,6 @@ Instance relation_disjunction_morphism : Proper (relation_equivalence (A:=A) ==>
 
 (* Predicate equivalence is exactly the same as the pointwise lifting of [iff]. *)
 
-Require Import List.
-
 Lemma predicate_equivalence_pointwise (l : Tlist) :
   Proper (@predicate_equivalence l ==> pointwise_lifting iff l) id.
 Proof. do 2 red. unfold predicate_equivalence. auto. Qed.
@@ -40,7 +38,7 @@ Lemma predicate_implication_pointwise (l : Tlist) :
   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
+(** The instantiation at relation allows rewriting applications of relations
     [R x y] to [R' x y]  when [R] and [R'] are in [relation_equivalence]. *)
 
 Instance relation_equivalence_pointwise :
@@ -52,6 +50,6 @@ Instance subrelation_pointwise :
 Proof. intro. apply (predicate_implication_pointwise (Tcons A (Tcons A Tnil))). Qed.
 
 
-Lemma inverse_pointwise_relation A (R : relation A) :
-  relation_equivalence (pointwise_relation A (inverse R)) (inverse (pointwise_relation A R)).
+Lemma flip_pointwise_relation A (R : relation A) :
+  relation_equivalence (pointwise_relation A (flip R)) (flip (pointwise_relation A R)).
 Proof. intros. split; firstorder. Qed.
diff --git a/theories/Classes/RelationClasses.v b/theories/Classes/RelationClasses.v
index 5c4dd532..1a40e5d5 100644
--- a/theories/Classes/RelationClasses.v
+++ b/theories/Classes/RelationClasses.v
@@ -1,7 +1,7 @@
 (* -*- coding: utf-8 -*- *)
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -20,43 +20,191 @@ Require Import Coq.Program.Basics.
 Require Import Coq.Program.Tactics.
 Require Import Coq.Relations.Relation_Definitions.
 
-(** We allow to unfold the [relation] definition while doing morphism search. *)
-
-Notation inverse R := (flip (R:relation _) : relation _).
-
-Definition complement {A} (R : relation A) : relation A := fun x y => R x y -> False.
-
-(** Opaque for proof-search. *)
-Typeclasses Opaque complement.
-
-(** These are convertible. *)
-
-Lemma complement_inverse : forall A (R : relation A), complement (inverse R) = inverse (complement R).
-Proof. reflexivity. Qed.
+Generalizable Variables A B C D R S T U l eqA eqB eqC eqD.
 
-(** We rebind relations in separate classes to be able to overload each proof. *)
+(** We allow to unfold the [relation] definition while doing morphism search. *)
 
-Set Implicit Arguments.
-Unset Strict Implicit.
+Section Defs.
+  Context {A : Type}.
+
+  (** We rebind relational properties in separate classes to be able to overload each proof. *)
+
+  Class Reflexive (R : relation A) :=
+    reflexivity : forall x : A, R x x.
+
+  Definition complement (R : relation A) : relation A := fun x y => R x y -> False.
+
+  (** Opaque for proof-search. *)
+  Typeclasses Opaque complement.
+  
+  (** These are convertible. *)
+  Lemma complement_inverse R : complement (flip R) = flip (complement R).
+  Proof. reflexivity. Qed.
+
+  Class Irreflexive (R : relation A) :=
+    irreflexivity : Reflexive (complement R).
+
+  Class Symmetric (R : relation A) :=
+    symmetry : forall {x y}, R x y -> R y x.
+  
+  Class Asymmetric (R : relation A) :=
+    asymmetry : forall {x y}, R x y -> R y x -> False.
+  
+  Class Transitive (R : relation A) :=
+    transitivity : forall {x y z}, R x y -> R y z -> R x z.
+
+  (** Various combinations of reflexivity, symmetry and transitivity. *)
+  
+  (** A [PreOrder] is both Reflexive and Transitive. *)
+  
+  Class PreOrder (R : relation A) : Prop := {
+    PreOrder_Reflexive :> Reflexive R | 2 ;
+    PreOrder_Transitive :> Transitive R | 2 }.
+
+  (** A [StrictOrder] is both Irreflexive and Transitive. *)
+
+  Class StrictOrder (R : relation A) : Prop := {
+    StrictOrder_Irreflexive :> Irreflexive R ;
+    StrictOrder_Transitive :> Transitive R }.
+
+  (** By definition, a strict order is also asymmetric *)
+  Global Instance StrictOrder_Asymmetric `(StrictOrder R) : Asymmetric R.
+  Proof. firstorder. Qed.
+
+  (** A partial equivalence relation is Symmetric and Transitive. *)
+  
+  Class PER (R : relation A) : Prop := {
+    PER_Symmetric :> Symmetric R | 3 ;
+    PER_Transitive :> Transitive R | 3 }.
+
+  (** Equivalence relations. *)
+
+  Class Equivalence (R : relation A) : Prop := {
+    Equivalence_Reflexive :> Reflexive R ;
+    Equivalence_Symmetric :> Symmetric R ;
+    Equivalence_Transitive :> Transitive R }.
+
+  (** An Equivalence is a PER plus reflexivity. *)
+  
+  Global Instance Equivalence_PER {R} `(E:Equivalence R) : PER R | 10 :=
+    { }. 
+
+  (** We can now define antisymmetry w.r.t. an equivalence relation on the carrier. *)
+  
+  Class Antisymmetric eqA `{equ : Equivalence eqA} (R : relation A) :=
+    antisymmetry : forall {x y}, R x y -> R y x -> eqA x y.
+
+  Class subrelation (R R' : relation A) : Prop :=
+    is_subrelation : forall {x y}, R x y -> R' x y.
+  
+  (** Any symmetric relation is equal to its inverse. *)
+  
+  Lemma subrelation_symmetric R `(Symmetric R) : subrelation (flip R) R.
+  Proof. hnf. intros. red in H0. apply symmetry. assumption. Qed.
+
+  Section flip.
+  
+    Lemma flip_Reflexive `{Reflexive R} : Reflexive (flip R).
+    Proof. tauto. Qed.
+    
+    Program Definition flip_Irreflexive `(Irreflexive R) : Irreflexive (flip R) :=
+      irreflexivity (R:=R).
+    
+    Program Definition flip_Symmetric `(Symmetric R) : Symmetric (flip R) :=
+      fun x y H => symmetry (R:=R) H.
+    
+    Program Definition flip_Asymmetric `(Asymmetric R) : Asymmetric (flip R) :=
+      fun x y H H' => asymmetry (R:=R) H H'.
+    
+    Program Definition flip_Transitive `(Transitive R) : Transitive (flip R) :=
+      fun x y z H H' => transitivity (R:=R) H' H.
+
+    Program Definition flip_Antisymmetric `(Antisymmetric eqA R) :
+      Antisymmetric eqA (flip R).
+    Proof. firstorder. Qed.
+
+    (** Inversing the larger structures *)
+
+    Lemma flip_PreOrder `(PreOrder R) : PreOrder (flip R).
+    Proof. firstorder. Qed.
+
+    Lemma flip_StrictOrder `(StrictOrder R) : StrictOrder (flip R).
+    Proof. firstorder. Qed.
+
+    Lemma flip_PER `(PER R) : PER (flip R).
+    Proof. firstorder. Qed.
+
+    Lemma flip_Equivalence `(Equivalence R) : Equivalence (flip R).
+    Proof. firstorder. Qed.
+
+  End flip.
+
+  Section complement.
+
+    Definition complement_Irreflexive `(Reflexive R)
+      : Irreflexive (complement R).
+    Proof. firstorder. Qed.
+
+    Definition complement_Symmetric `(Symmetric R) : Symmetric (complement R).
+    Proof. firstorder. Qed.
+  End complement.
+
+
+  (** 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 Reflexive {A} (R : relation A) :=
-  reflexivity : forall x, R x x.
+  Class RewriteRelation (RA : relation A).
 
-Class Irreflexive {A} (R : relation A) :=
-  irreflexivity : Reflexive (complement R).
+  (** Any [Equivalence] declared in the context is automatically considered
+   a rewrite relation. *)
+    
+  Global Instance equivalence_rewrite_relation `(Equivalence eqA) : RewriteRelation eqA.
+
+  (** Leibniz equality. *)
+  Section Leibniz.
+    Global Instance eq_Reflexive : Reflexive (@eq A) := @eq_refl A.
+    Global Instance eq_Symmetric : Symmetric (@eq A) := @eq_sym A.
+    Global Instance eq_Transitive : Transitive (@eq A) := @eq_trans A.
+    
+    (** Leibinz equality [eq] is an equivalence relation.
+        The instance has low priority as it is always applicable
+        if only the type is constrained. *)
+    
+    Global Program Instance eq_equivalence : Equivalence (@eq A) | 10.
+  End Leibniz.
+  
+End Defs.
+
+(** Default rewrite relations handled by [setoid_rewrite]. *)
+Instance: RewriteRelation impl.
+Instance: RewriteRelation iff.
 
+(** Hints to drive the typeclass resolution avoiding loops
+ due to the use of full unification. *)
 Hint Extern 1 (Reflexive (complement _)) => class_apply @irreflexivity : typeclass_instances.
+Hint Extern 3 (Symmetric (complement _)) => class_apply complement_Symmetric : typeclass_instances.
+Hint Extern 3 (Irreflexive (complement _)) => class_apply complement_Irreflexive : typeclass_instances.
 
-Class Symmetric {A} (R : relation A) :=
-  symmetry : forall x y, R x y -> R y x.
+Hint Extern 3 (Reflexive (flip _)) => apply flip_Reflexive : typeclass_instances.
+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 (Antisymmetric (flip _)) => class_apply flip_Antisymmetric : typeclass_instances.
+Hint Extern 3 (Transitive (flip _)) => class_apply flip_Transitive : typeclass_instances.
+Hint Extern 3 (StrictOrder (flip _)) => class_apply flip_StrictOrder : typeclass_instances.
+Hint Extern 3 (PreOrder (flip _)) => class_apply flip_PreOrder : typeclass_instances.
 
-Class Asymmetric {A} (R : relation A) :=
-  asymmetry : forall x y, R x y -> R y x -> False.
+Hint Extern 4 (subrelation (flip _) _) => 
+  class_apply @subrelation_symmetric : typeclass_instances.
 
-Class Transitive {A} (R : relation A) :=
-  transitivity : forall x y z, R x y -> R y z -> R x z.
+Arguments irreflexivity {A R Irreflexive} [x] _.
 
-Hint Resolve @irreflexivity : ord.
+Hint Resolve irreflexivity : ord.
 
 Unset Implicit Arguments.
 
@@ -72,40 +220,6 @@ Hint Extern 4 => solve_relation : relations.
 
 (** We can already dualize all these properties. *)
 
-Generalizable Variables A B C D R S T U l eqA eqB eqC eqD.
-
-Lemma flip_Reflexive `{Reflexive A R} : Reflexive (flip R).
-Proof. tauto. Qed.
-
-Hint Extern 3 (Reflexive (flip _)) => apply flip_Reflexive : typeclass_instances.
-
-Program Definition flip_Irreflexive `(Irreflexive A R) : Irreflexive (flip R) :=
-  irreflexivity (R:=R).
-
-Program Definition flip_Symmetric `(Symmetric A R) : Symmetric (flip R) :=
-  fun x y H => symmetry (R:=R) H.
-
-Program Definition flip_Asymmetric `(Asymmetric A R) : Asymmetric (flip R) :=
-  fun x y H H' => asymmetry (R:=R) H H'.
-
-Program Definition flip_Transitive `(Transitive A R) : Transitive (flip R) :=
-  fun x y z H H' => transitivity (R:=R) H' H.
-
-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.
-
-Definition Reflexive_complement_Irreflexive `(Reflexive A (R : relation A))
-   : Irreflexive (complement R).
-Proof. firstorder. Qed.
-
-Definition complement_Symmetric `(Symmetric A (R : relation A)) : Symmetric (complement R).
-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. *)
 
 Ltac reduce_hyp H :=
@@ -130,7 +244,7 @@ Tactic Notation "apply" "*" constr(t) :=
 
 Ltac simpl_relation :=
   unfold flip, impl, arrow ; try reduce ; program_simpl ;
-    try ( solve [ intuition ]).
+    try ( solve [ dintuition ]).
 
 Local Obligation Tactic := simpl_relation.
 
@@ -145,54 +259,6 @@ Instance iff_Reflexive : Reflexive iff := iff_refl.
 Instance iff_Symmetric : Symmetric iff := iff_sym.
 Instance iff_Transitive : Transitive iff := iff_trans.
 
-(** Leibniz equality. *)
-
-Instance eq_Reflexive {A} : Reflexive (@eq A) := @eq_refl A.
-Instance eq_Symmetric {A} : Symmetric (@eq A) := @eq_sym A.
-Instance eq_Transitive {A} : Transitive (@eq A) := @eq_trans A.
-
-(** Various combinations of reflexivity, symmetry and transitivity. *)
-
-(** A [PreOrder] is both Reflexive and Transitive. *)
-
-Class PreOrder {A} (R : relation A) : Prop := {
-  PreOrder_Reflexive :> Reflexive R | 2 ;
-  PreOrder_Transitive :> Transitive R | 2 }.
-
-(** A partial equivalence relation is Symmetric and Transitive. *)
-
-Class PER {A} (R : relation A) : Prop := {
-  PER_Symmetric :> Symmetric R | 3 ;
-  PER_Transitive :> Transitive R | 3 }.
-
-(** Equivalence relations. *)
-
-Class Equivalence {A} (R : relation A) : Prop := {
-  Equivalence_Reflexive :> Reflexive R ;
-  Equivalence_Symmetric :> Symmetric R ;
-  Equivalence_Transitive :> Transitive R }.
-
-(** An Equivalence is a PER plus reflexivity. *)
-
-Instance Equivalence_PER `(Equivalence A R) : PER R | 10 :=
-  { PER_Symmetric := Equivalence_Symmetric ;
-    PER_Transitive := Equivalence_Transitive }.
-
-(** 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.
-
-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
-   if only the type is constrained. *)
-
-Program Instance eq_equivalence : Equivalence (@eq A) | 10.
-
 (** Logical equivalence [iff] is an equivalence relation. *)
 
 Program Instance iff_equivalence : Equivalence iff.
@@ -203,9 +269,6 @@ Program Instance iff_equivalence : Equivalence iff.
 
 Local Open Scope list_scope.
 
-(* Notation " [ ] " := nil : list_scope. *)
-(* Notation " [ x ; .. ; y ] " := (cons x .. (cons y nil) ..) (at level 1) : list_scope. *)
-
 (** A compact representation of non-dependent arities, with the codomain singled-out. *)
 
 (* Note, we do not use [list Type] because it imposes unnecessary universe constraints *)
@@ -316,7 +379,8 @@ 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.
@@ -345,106 +409,66 @@ Program Instance predicate_implication_preorder :
 (** 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 (_::_::Tnil).
-
-Class subrelation {A:Type} (R R' : relation A) : Prop :=
-  is_subrelation : @predicate_implication (A::A::Tnil) R R'.
-
-Arguments subrelation {A} R R'.
-
-Definition relation_conjunction {A} (R : relation A) (R' : relation A) : relation A :=
-  @predicate_intersection (A::A::Tnil) R R'.
-
-Definition relation_disjunction {A} (R : relation A) (R' : relation A) : relation A :=
-  @predicate_union (A::A::Tnil) 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. exact (@predicate_equivalence_equivalence (A::A::Tnil)). Qed.
-
-Instance relation_implication_preorder A : PreOrder (@subrelation A).
-Proof. exact (@predicate_implication_preorder (A::A::Tnil)). Qed.
-
-(** *** Partial Order.
+Section Binary.
+  Context {A : Type}.
+
+  Definition relation_equivalence : relation (relation A) :=
+    @predicate_equivalence (_::_::Tnil).
+
+  Global Instance: RewriteRelation relation_equivalence.
+  
+  Definition relation_conjunction (R : relation A) (R' : relation A) : relation A :=
+    @predicate_intersection (A::A::Tnil) R R'.
+
+  Definition relation_disjunction (R : relation A) (R' : relation A) : relation A :=
+    @predicate_union (A::A::Tnil) R R'.
+  
+  (** Relation equivalence is an equivalence, and subrelation defines a partial order. *)
+  
+  Set Automatic Introduction.
+  
+  Global Instance relation_equivalence_equivalence :
+    Equivalence relation_equivalence.
+  Proof. exact (@predicate_equivalence_equivalence (A::A::Tnil)). Qed.
+  
+  Global Instance relation_implication_preorder : PreOrder (@subrelation A).
+  Proof. exact (@predicate_implication_preorder (A::A::Tnil)). Qed.
+
+  (** *** Partial Order.
    A partial order is a preorder which is additionally antisymmetric.
    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)).
+  Class PartialOrder eqA `{equ : Equivalence A eqA} R `{preo : PreOrder A R} :=
+    partial_order_equivalence : relation_equivalence eqA (relation_conjunction R (flip R)).
+  
+  (** 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] *)
+
+  Global Instance partial_order_antisym `(PartialOrder eqA R) : ! Antisymmetric A eqA R.
+  Proof with auto.
+    reduce_goal.
+    pose proof partial_order_equivalence as poe. do 3 red in poe.
+    apply <- poe. firstorder.
+  Qed.
 
-(** 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.
-  apply <- poe. firstorder.
-Qed.
+  Lemma PartialOrder_inverse `(PartialOrder eqA R) : PartialOrder eqA (flip R).
+  Proof. firstorder. Qed.
+End Binary.
+
+Hint Extern 3 (PartialOrder (flip _)) => class_apply PartialOrder_inverse : typeclass_instances.
 
 (** The partial order defined by subrelation and relation equivalence. *)
 
 Program Instance subrelation_partial_order :
   ! PartialOrder (relation A) relation_equivalence subrelation.
 
-  Next Obligation.
-  Proof.
-    unfold relation_equivalence in *. compute; firstorder.
-  Qed.
+Next Obligation.
+Proof.
+  unfold relation_equivalence in *. compute; firstorder.
+Qed.
 
 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) : Prop := {
-  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.
+            relation_equivalence pointwise_lifting.
diff --git a/theories/Classes/RelationPairs.v b/theories/Classes/RelationPairs.v
index 2b010206..cbde5f9a 100644
--- a/theories/Classes/RelationPairs.v
+++ b/theories/Classes/RelationPairs.v
@@ -9,8 +9,8 @@
 (** * Relations over pairs *)
 
 
+Require Import SetoidList.
 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.
@@ -40,7 +40,7 @@ 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 :=
+Definition RelCompFun {A} {B : Type}(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.
@@ -62,13 +62,13 @@ 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).
+Definition RelProd {A : Type} {B : Type} (RA:relation A)(RB:relation B) : relation (A*B) :=
+ relation_conjunction (@RelCompFun (A * B) A RA fst) (RB @@2).
 
 Infix "*" := RelProd : signature_scope.
 
 Section RelCompFun_Instances.
-  Context {A B : Type} (R : relation B).
+  Context {A : Type} {B : Type} (R : relation B).
 
   Global Instance RelCompFun_Reflexive
     `(Measure A B f, Reflexive _ R) : Reflexive (R@@f).
@@ -94,57 +94,61 @@ Section RelCompFun_Instances.
 
 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.
-
-Program 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.
+Section RelProd_Instances.
+
+  Context {A : Type} {B : Type} (RA : relation A) (RB : relation B).
+
+  Global Instance RelProd_Reflexive `(Reflexive _ RA, Reflexive _ RB) : Reflexive (RA*RB).
+  Proof. firstorder. Qed.
+
+  Global Instance RelProd_Symmetric `(Symmetric _ RA, Symmetric _ RB)
+  : Symmetric (RA*RB).
+  Proof. firstorder. Qed.
+
+  Global Instance RelProd_Transitive 
+           `(Transitive _ RA, Transitive _ RB) : Transitive (RA*RB).
+  Proof. firstorder. Qed.
+
+  Global Program Instance RelProd_Equivalence 
+          `(Equivalence _ RA, Equivalence _ RB) : Equivalence (RA*RB).
+
+  Lemma FstRel_ProdRel :
+    relation_equivalence (RA @@1) (RA*(fun _ _ : B => True)).
+  Proof. firstorder. Qed.
+  
+  Lemma SndRel_ProdRel :
+    relation_equivalence (RB @@2) ((fun _ _ : A =>True) * RB).
+  Proof. firstorder. Qed.
+  
+  Global Instance FstRel_sub :
+    subrelation (RA*RB) (RA @@1).
+  Proof. firstorder. Qed.
+
+  Global Instance SndRel_sub :
+    subrelation (RA*RB) (RB @@2).
+  Proof. firstorder. Qed.
+  
+  Global Instance pair_compat :
+    Proper (RA==>RB==> RA*RB) (@pair _ _).
+  Proof. firstorder. Qed.
+  
+  Global Instance fst_compat :
+    Proper (RA*RB ==> RA) Fst.
+  Proof.
+    intros (x,y) (x',y') (Hx,Hy); compute in *; auto.
+  Qed.
+
+  Global Instance snd_compat :
+    Proper (RA*RB ==> RB) Snd.
+  Proof.
+    intros (x,y) (x',y') (Hx,Hy); compute in *; auto.
+  Qed.
+
+  Global Instance RelCompFun_compat (f:A->B)
+           `(Proper _ (Ri==>Ri==>Ro) RB) :
+    Proper (Ri@@f==>Ri@@f==>Ro) (RB@@f)%signature.
+  Proof. unfold RelCompFun; firstorder. Qed.
+End RelProd_Instances.
 
 Hint Unfold RelProd RelCompFun.
 Hint Extern 2 (RelProd _ _ _ _) => split.
diff --git a/theories/Classes/SetoidClass.v b/theories/Classes/SetoidClass.v
index e7b94081..f20100fe 100644
--- a/theories/Classes/SetoidClass.v
+++ b/theories/Classes/SetoidClass.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/theories/Classes/SetoidDec.v b/theories/Classes/SetoidDec.v
index 79168084..bf05934e 100644
--- a/theories/Classes/SetoidDec.v
+++ b/theories/Classes/SetoidDec.v
@@ -1,7 +1,7 @@
 (* -*- coding: utf-8 -*- *)
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -108,7 +108,7 @@ Program Instance prod_eqdec `(! EqDec (eq_setoid A), ! EqDec (eq_setoid B))
       else in_right
     else in_right.
 
-  Solve Obligations using unfold complement ; program_simpl.
+  Solve Obligations with unfold complement ; program_simpl.
 
 (** Objects of function spaces with countable domains like bool
   have decidable equality. *)
@@ -121,7 +121,7 @@ Program Instance bool_function_eqdec `(! EqDec (eq_setoid A))
       else in_right
     else in_right.
 
-  Solve Obligations using try red ; unfold equiv, complement ; program_simpl.
+  Solve Obligations with try red ; unfold complement ; program_simpl.
 
   Next Obligation.
   Proof.
diff --git a/theories/Classes/SetoidTactics.v b/theories/Classes/SetoidTactics.v
index 07d1203c..8ca93341 100644
--- a/theories/Classes/SetoidTactics.v
+++ b/theories/Classes/SetoidTactics.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -12,6 +12,7 @@
    Institution: LRI, CNRS UMR 8623 - University Paris Sud
 *)
 
+Require Coq.Classes.CRelationClasses Coq.Classes.CMorphisms.
 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.
diff --git a/theories/Classes/vo.itarget b/theories/Classes/vo.itarget
index 9daf133b..18147f2a 100644
--- a/theories/Classes/vo.itarget
+++ b/theories/Classes/vo.itarget
@@ -1,3 +1,4 @@
+DecidableClass.vo
 Equivalence.vo
 EquivDec.vo
 Init.vo
@@ -9,3 +10,6 @@ SetoidClass.vo
 SetoidDec.vo
 SetoidTactics.vo
 RelationPairs.vo
+CRelationClasses.vo
+CMorphisms.vo
+CEquivalence.vo