11 files changed, 213 insertions, 175 deletions

diff --git a/theories/Classes/EquivDec.v b/theories/Classes/EquivDec.v
index debe953a..1e58d05d 100644
--- a/theories/Classes/EquivDec.v
+++ b/theories/Classes/EquivDec.v
@@ -13,7 +13,7 @@
  * Institution: LRI, CNRS UMR 8623 - UniversitĂcopyright Paris Sud
  *              91405 Orsay, France *)
 
-(* $Id: EquivDec.v 10919 2008-05-11 22:04:26Z msozeau $ *)
+(* $Id: EquivDec.v 11282 2008-07-28 11:51:53Z msozeau $ *)
 
 Set Implicit Arguments.
 Unset Strict Implicit.
@@ -40,7 +40,7 @@ Class [ equiv : Equivalence A ] => EqDec :=
 (** We define the [==] overloaded notation for deciding equality. It does not take precedence
    of [==] defined in the type scope, hence we can have both at the same time. *)
 
-Notation " x == y " := (equiv_dec (x :>) (y :>)) (no associativity, at level 70).
+Notation " x == y " := (equiv_dec (x :>) (y :>)) (no associativity, at level 70) : equiv_scope.
 
 Definition swap_sumbool {A B} (x : { A } + { B }) : { B } + { A } :=
   match x with
@@ -58,7 +58,7 @@ Program Definition nequiv_dec [ EqDec A ] (x y : A) : { x =/= y } + { x === y }
 
 (** Overloaded notation for inequality. *)
 
-Infix "=/=" := nequiv_dec (no associativity, at level 70).
+Infix "<>" := nequiv_dec (no associativity, at level 70) : equiv_scope.
 
 (** Define boolean versions, losing the logical information. *)
 
@@ -155,4 +155,4 @@ Program Instance list_eqdec [ eqa : EqDec A eq ] : ! EqDec (list A) eq :=
   Next Obligation.
   Proof. clear aux. red in H0. subst. 
     destruct y; intuition (discriminate || eauto).
-  Defined.
\ No newline at end of file
+  Defined.
diff --git a/theories/Classes/Equivalence.v b/theories/Classes/Equivalence.v
index 70bf3483..d52eed47 100644
--- a/theories/Classes/Equivalence.v
+++ b/theories/Classes/Equivalence.v
@@ -13,7 +13,7 @@
    Institution: LRI, CNRS UMR 8623 - UniversitĂcopyright Paris Sud
    91405 Orsay, France *) 
 
-(* $Id: Equivalence.v 10919 2008-05-11 22:04:26Z msozeau $ *)
+(* $Id: Equivalence.v 11282 2008-07-28 11:51:53Z msozeau $ *)
 
 Require Export Coq.Program.Basics.
 Require Import Coq.Program.Tactics.
@@ -116,7 +116,7 @@ Section Respecting.
   Definition respecting [ Equivalence A (R : relation A), Equivalence B (R' : relation B) ] : Type := 
     { morph : A -> B | respectful R R' morph morph }.
   
-  Program Instance respecting_equiv [ Equivalence A R, Equivalence B R' ] :
+  Program Instance respecting_equiv [ eqa : Equivalence A R, eqb : Equivalence B R' ] :
     Equivalence respecting
     (fun (f g : respecting) => forall (x y : A), R x y -> R' (proj1_sig f x) (proj1_sig g y)).
 
@@ -124,18 +124,17 @@ Section Respecting.
 
   Next Obligation.
   Proof. 
-    unfold respecting in *. program_simpl. red in H2,H3,H4. 
-    transitivity (y x0) ; auto.
-    transitivity (y y0) ; auto.
-    symmetry. auto.
+    unfold respecting in *. program_simpl. transitivity (y y0); auto. apply H0. reflexivity.
   Qed.
 
 End Respecting.
 
 (** The default equivalence on function spaces, with higher-priority than [eq]. *)
 
-Program Instance pointwise_equivalence [ Equivalence A eqA ] :
-  Equivalence (B -> A) (pointwise_relation eqA) | 9.
+Program Instance pointwise_equivalence [ eqb : Equivalence B eqB ] :
+  Equivalence (A -> B) (pointwise_relation eqB) | 9.
+
+  Solve Obligations using simpl_relation ; first [ reflexivity | (symmetry ; auto) ].
 
   Next Obligation.
   Proof.
diff --git a/theories/Classes/Functions.v b/theories/Classes/Functions.v
index 49fc4f89..4c844911 100644
--- a/theories/Classes/Functions.v
+++ b/theories/Classes/Functions.v
@@ -13,7 +13,7 @@
    Institution: LRI, CNRS UMR 8623 - UniversitÃcopyright Paris Sud
    91405 Orsay, France *)
 
-(* $Id: Functions.v 10739 2008-04-01 14:45:20Z herbelin $ *)
+(* $Id: Functions.v 11282 2008-07-28 11:51:53Z msozeau $ *)
 
 Require Import Coq.Classes.RelationClasses.
 Require Import Coq.Classes.Morphisms.
@@ -21,22 +21,22 @@ Require Import Coq.Classes.Morphisms.
 Set Implicit Arguments.
 Unset Strict Implicit.
 
-Class [ m : Morphism (A -> B) (RA ++> RB) f ] => Injective : Prop :=
+Class Injective ((m : Morphism (A -> B) (RA ++> RB) f)) : Prop :=
   injective : forall x y : A, RB (f x) (f y) -> RA x y.
 
-Class [ m : Morphism (A -> B) (RA ++> RB) f ] => Surjective : Prop :=
+Class ((m : Morphism (A -> B) (RA ++> RB) f)) => Surjective : Prop :=
   surjective : forall y, exists x : A, RB y (f x).
 
-Definition Bijective [ m : Morphism (A -> B) (RA ++> RB) (f : A -> B) ] :=
+Definition Bijective ((m : Morphism (A -> B) (RA ++> RB) (f : A -> B))) :=
   Injective m /\ Surjective m.
 
-Class [ m : Morphism (A -> B) (eqA ++> eqB) ] => MonoMorphism :=
+Class MonoMorphism (( m : Morphism (A -> B) (eqA ++> eqB) )) :=
   monic :> Injective m.
 
-Class [ m : Morphism (A -> B) (eqA ++> eqB) ] => EpiMorphism :=
+Class EpiMorphism ((m : Morphism (A -> B) (eqA ++> eqB))) :=
   epic :> Surjective m.
 
-Class [ m : Morphism (A -> B) (eqA ++> eqB) ] => IsoMorphism :=
+Class IsoMorphism ((m : Morphism (A -> B) (eqA ++> eqB))) :=
   monomorphism :> MonoMorphism m ; epimorphism :> EpiMorphism m.
 
-Class [ m : Morphism (A -> A) (eqA ++> eqA), ! IsoMorphism m ] => AutoMorphism.
+Class ((m : Morphism (A -> A) (eqA ++> eqA))) [ ! IsoMorphism m ] => AutoMorphism.
diff --git a/theories/Classes/Init.v b/theories/Classes/Init.v
index 6ba0c61e..e5f951d0 100644
--- a/theories/Classes/Init.v
+++ b/theories/Classes/Init.v
@@ -13,9 +13,22 @@
    Institution: LRI, CNRS UMR 8623 - UniversitÃcopyright Paris Sud
    91405 Orsay, France *)
 
-(* $Id: Init.v 10739 2008-04-01 14:45:20Z herbelin $ *)
+(* $Id: Init.v 11282 2008-07-28 11:51:53Z msozeau $ *)
 
 (* Ltac typeclass_instantiation := typeclasses eauto || eauto. *)
 
 Tactic Notation "clapply" ident(c) :=
   eapply @c ; eauto with typeclass_instances.
+
+(** The unconvertible typeclass, to test that two objects of the same type are 
+   actually different. *)
+
+Class Unconvertible (A : Type) (a b : A).
+
+Ltac unconvertible :=
+  match goal with
+    | |- @Unconvertible _ ?x ?y => conv x y ; fail 1 "Convertible"
+    | |- _ => apply Build_Unconvertible 
+  end.
+
+Hint Extern 0 (@Unconvertible _ _ _) => unconvertible : typeclass_instances.
\ No newline at end of file
diff --git a/theories/Classes/Morphisms.v b/theories/Classes/Morphisms.v
index f21c68a6..c2ae026d 100644
--- a/theories/Classes/Morphisms.v
+++ b/theories/Classes/Morphisms.v
@@ -1,4 +1,4 @@
-(* -*- coq-prog-args: ("-emacs-U" "-top" "Coq.Classes.Morphisms"); compile-command: "make -C ../.. TIME='time'" -*- *)
+(* -*- coq-prog-name: "~/research/coq/trunk/bin/coqtop.byte"; coq-prog-args: ("-emacs-U" "-top" "Coq.Classes.Morphisms"); compile-command: "make -C ../.. TIME='time'" -*- *)
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
 (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
@@ -13,7 +13,7 @@
    Institution: LRI, CNRS UMR 8623 - UniversitÃcopyright Paris Sud
    91405 Orsay, France *)
 
-(* $Id: Morphisms.v 11092 2008-06-10 18:28:26Z msozeau $ *)
+(* $Id: Morphisms.v 11282 2008-07-28 11:51:53Z msozeau $ *)
 
 Require Import Coq.Program.Basics.
 Require Import Coq.Program.Tactics.
@@ -39,10 +39,6 @@ Class Morphism A (R : relation A) (m : A) : Prop :=
 
 Implicit Arguments Morphism [A].
 
-(** We allow to unfold the [relation] definition while doing morphism search. *)
-
-Typeclasses unfold relation.
-
 (** Respectful morphisms. *)
 
 (** The fully dependent version, not used yet. *)
@@ -79,9 +75,22 @@ Arguments Scope respectful [type_scope type_scope signature_scope signature_scop
 
 Open Local Scope signature_scope.
 
+(** Pointwise lifting is just respect with leibniz equality on the left. *)
+
+Definition pointwise_relation {A B : Type} (R : relation B) : relation (A -> B) := 
+  fun f g => forall x : A, R (f x) (g x).
+
+Lemma pointwise_pointwise A B (R : relation B) : 
+  relation_equivalence (pointwise_relation 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. *)
 
+Hint Unfold Reflexive : core.
+Hint Unfold Symmetric : core.
+Hint Unfold Transitive : core.
+
 Program Instance respectful_per [ PER A (R : relation A), PER B (R' : relation B) ] : 
   PER (A -> B) (R ==> R').
 
@@ -92,24 +101,26 @@ Program Instance respectful_per [ PER A (R : relation A), PER B (R' : relation B
     transitivity (y x0)...
   Qed.
 
-(** Subrelations induce a morphism on the identity, not used for morphism search yet. *)
+(** Subrelations induce a morphism on the identity. *)
 
-Lemma subrelation_id_morphism [ subrelation A R₁ R₂ ] : Morphism (R₁ ==> R₂) id.
+Instance subrelation_id_morphism [ subrelation A R₁ R₂ ] : Morphism (R₁ ==> R₂) id.
 Proof. firstorder. Qed.
 
 (** The subrelation property goes through products as usual. *)
 
-Instance morphisms_subrelation [ sub : subrelation A R₁ R₂ ] :
-  ! subrelation (B -> A) (R ==> R₁) (R ==> R₂).
-Proof. firstorder. Qed.
+Instance morphisms_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.
 
-Instance morphisms_subrelation_left [ sub : subrelation A R₂ R₁ ] :
-  ! subrelation (A -> B) (R₁ ==> R) (R₂ ==> R) | 3.
-Proof. firstorder. Qed.
+(** And of course it is reflexive. *)
+
+Instance morphisms_subrelation_refl : ! subrelation A R R | 10.
+Proof. simpl_relation. Qed.
 
 (** [Morphism] is itself a covariant morphism for [subrelation]. *)
 
-Lemma subrelation_morphism [ sub : subrelation A R₁ R₂, mor : Morphism A R₁ m ] : Morphism R₂ m.
+Lemma subrelation_morphism [ mor : Morphism A R₁ m, unc : Unconvertible (relation A) R₁ R₂,
+  sub : subrelation A R₁ R₂ ] : Morphism R₂ m.
 Proof.
   intros. apply sub. apply mor.
 Qed.
@@ -121,8 +132,9 @@ Proof. reduce. subst. firstorder. Qed.
 (** We use an external tactic to manage the application of subrelation, which is otherwise
    always applicable. We allow its use only once per branch. *)
 
-Inductive subrelation_done : Prop :=
-  did_subrelation : subrelation_done.
+Inductive subrelation_done : Prop := did_subrelation : subrelation_done.
+
+Inductive normalization_done : Prop := did_normalization.
 
 Ltac subrelation_tac := 
   match goal with
@@ -131,7 +143,7 @@ Ltac subrelation_tac :=
       set(H:=did_subrelation) ; eapply @subrelation_morphism
   end.
 
-Hint Extern 4 (@Morphism _ _ _) => subrelation_tac : typeclass_instances.
+Hint Extern 5 (@Morphism _ _ _) => subrelation_tac : typeclass_instances.
 
 (** Essential subrelation instances for [iff], [impl] and [pointwise_relation]. *)
 
@@ -181,20 +193,10 @@ Program Instance trans_contra_co_morphism
     transitivity x0...
   Qed.
 
-(* (** Dually... *) *)
-
-(* Program Instance [ Transitive A R ] => *)
-(*   trans_co_contra_inv_impl_morphism : Morphism (R ++> R --> inverse impl) R. *)
-  
-(*   Next Obligation. *)
-(*   Proof with auto. *)
-(*     apply* trans_contra_co_morphism ; eauto. eauto. *)
-(*   Qed. *)
-
 (** Morphism declarations for partial applications. *)
 
 Program Instance trans_contra_inv_impl_morphism
-  [ Transitive A R ] : Morphism (R --> inverse impl) (R x).
+  [ Transitive A R ] : Morphism (R --> inverse impl) (R x) | 3.
 
   Next Obligation.
   Proof with auto.
@@ -202,7 +204,7 @@ Program Instance trans_contra_inv_impl_morphism
   Qed.
 
 Program Instance trans_co_impl_morphism
-  [ Transitive A R ] : Morphism (R ==> impl) (R x).
+  [ Transitive A R ] : Morphism (R ==> impl) (R x) | 3.
 
   Next Obligation.
   Proof with auto.
@@ -210,23 +212,23 @@ Program Instance trans_co_impl_morphism
   Qed.
 
 Program Instance trans_sym_co_inv_impl_morphism
-  [ Transitive A R, Symmetric A R ] : Morphism (R ==> inverse impl) (R x).
+  [ PER A R ] : Morphism (R ==> inverse impl) (R x) | 2.
 
   Next Obligation.
   Proof with auto.
-    transitivity y...
+    transitivity y... symmetry...
   Qed.
 
 Program Instance trans_sym_contra_impl_morphism
-  [ Transitive A R, Symmetric _ R ] : Morphism (R --> impl) (R x).
+  [ PER A R ] : Morphism (R --> impl) (R x) | 2.
 
   Next Obligation.
   Proof with auto.
-    transitivity x0...
+    transitivity x0... symmetry...
   Qed.
 
-Program Instance equivalence_partial_app_morphism
-  [ Equivalence A R ] : Morphism (R ==> iff) (R x).
+Program Instance per_partial_app_morphism
+  [ PER A R ] : Morphism (R ==> iff) (R x) | 1.
 
   Next Obligation.
   Proof with auto.
@@ -240,36 +242,16 @@ Program Instance equivalence_partial_app_morphism
    to get an [R y z] goal. *)
 
 Program Instance trans_co_eq_inv_impl_morphism
-  [ Transitive A R ] : Morphism (R ==> (@eq A) ==> inverse impl) R.
+  [ Transitive A R ] : Morphism (R ==> (@eq A) ==> inverse impl) R | 2.
 
   Next Obligation.
   Proof with auto.
     transitivity y...
   Qed.
 
-(* Program Instance [ Transitive A R ] =>  *)
-(*   trans_contra_eq_impl_morphism : Morphism (R --> (@eq A) ==> impl) R. *)
-
-(*   Next Obligation. *)
-(*   Proof with auto. *)
-(*     transitivity x... *)
-(*   Qed. *)
-
 (** Every Symmetric and Transitive relation gives rise to an equivariant morphism. *)
 
-Program Instance trans_sym_morphism
-  [ Transitive A R, Symmetric _ R ] : Morphism (R ==> R ==> iff) R.
-
-  Next Obligation.
-  Proof with auto.
-    split ; intros.
-    transitivity x0... transitivity x...
-  
-    transitivity y... transitivity y0... 
-  Qed.
-
-Program Instance equiv_morphism [ Equivalence A R ] :
-  Morphism (R ==> R ==> iff) R.
+Program Instance PER_morphism [ PER A R ] : Morphism (R ==> R ==> iff) R | 1.
 
   Next Obligation.
   Proof with auto.
@@ -279,27 +261,21 @@ Program Instance equiv_morphism [ Equivalence A R ] :
     transitivity y... transitivity y0... symmetry...
   Qed.
 
-(** In case the rewrite happens at top level. *)
-
-Program Instance iff_inverse_impl_id :
-  Morphism (iff ==> inverse impl) id.
-
-Program Instance inverse_iff_inverse_impl_id :
-  Morphism (iff --> inverse impl) id.
+Lemma symmetric_equiv_inverse [ Symmetric A R ] : relation_equivalence R (flip R).
+Proof. firstorder. Qed.
   
-Program Instance iff_impl_id :
-  Morphism (iff ==> impl) id.
+Program Instance compose_morphism A B C R₀ R₁ R₂ :
+  Morphism ((R₁ ==> R₂) ==> (R₀ ==> R₁) ==> (R₀ ==> R₂)) (@compose A B C).
+
+  Next Obligation.
+  Proof.
+    simpl_relation.
+    unfold compose. apply H. apply H0. apply H1.
+  Qed.
 
-Program Instance inverse_iff_impl_id :
-  Morphism (iff --> impl) id.
-  
 (** Coq functions are morphisms for leibniz equality, 
    applied only if really needed. *)
 
-(* Instance (A : Type) [ Reflexive B R ] => *)
-(*   eq_reflexive_morphism : Morphism (@Logic.eq A ==> R) m | 3. *)
-(* Proof. simpl_relation. Qed. *)
-
 Instance reflexive_eq_dom_reflexive (A : Type) [ Reflexive B R' ] :
   Reflexive (@Logic.eq A ==> R').
 Proof. simpl_relation. Qed.
@@ -335,49 +311,81 @@ Class MorphismProxy A (R : relation A) (m : A) : Prop :=
   respect_proxy : R m m.
 
 Instance reflexive_morphism_proxy
-  [ Reflexive A R ] (x : A) : MorphismProxy A R x | 1.
+  [ Reflexive A R ] (x : A) : MorphismProxy R x | 1.
 Proof. firstorder. Qed.
 
 Instance morphism_morphism_proxy
-  [ Morphism A R x ] : MorphismProxy A R x | 2.
+  [ Morphism A R x ] : MorphismProxy R x | 2.
 Proof. firstorder. Qed.
 
-(* Instance (A : Type) [ Reflexive B R ] => *)
-(*   eq_reflexive_morphism : Morphism (@Logic.eq A ==> R) m | 3. *)
-(* Proof. simpl_relation. Qed. *)
-
 (** [R] is Reflexive, hence we can build the needed proof. *)
 
 Lemma Reflexive_partial_app_morphism [ Morphism (A -> B) (R ==> R') m, MorphismProxy A R x ] :
    Morphism R' (m x).
 Proof. simpl_relation. Qed.
 
+Class Params {A : Type} (of : A) (arity : nat).
+
+Class PartialApplication.
+
 Ltac partial_application_tactic := 
-  let tac x :=
-    match type of x with
-      | Type => fail 1
-      | _ => eapply @Reflexive_partial_app_morphism
+  let rec do_partial_apps H m :=
+    match m with
+      | ?m' ?x => eapply @Reflexive_partial_app_morphism ; [do_partial_apps H m'|clear H]
+      | _ => idtac
     end
   in
-  let on_morphism m :=
-    match m with
-      | ?m' ?x => tac x
-      | ?m' _ ?x => tac x
-      | ?m' _ _ ?x => tac x
-      | ?m' _ _ _ ?x => tac x
-      | ?m' _ _ _ _ ?x => tac x
-      | ?m' _ _ _ _ _ ?x => tac x
-      | ?m' _ _ _ _ _ _ ?x => tac x
-      | ?m' _ _ _ _ _ _ _ ?x => tac x
-      | ?m' _ _ _ _ _ _ _ _ ?x => tac x
+  let rec do_partial H ar m :=
+    match ar with
+      | 0 => do_partial_apps H m
+      | S ?n' => 
+        match m with
+          ?m' ?x => do_partial H n' m'
+        end
     end
   in
+  let on_morphism m :=
+    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 
+      do_partial H v' m
+ in
   match goal with
-    | [ |- @Morphism _ _ ?m ] => on_morphism m
+    | [ _ : subrelation_done |- _ ] => fail 1
+    | [ _ : normalization_done |- _ ] => fail 1
+    | [ _ : @Params _ _ _ |- _ ] => fail 1
+    | [ |- @Morphism ?T _ (?m ?x) ] => 
+      match goal with 
+        | [ _ : PartialApplication |- _ ] => 
+          eapply @Reflexive_partial_app_morphism
+        | _ => 
+          on_morphism (m x) || 
+            (eapply @Reflexive_partial_app_morphism ;
+              [ pose Build_PartialApplication | idtac ])
+      end
   end.
 
-(* Program Instance [ Morphism (A -> B) (R ==> R') m, Reflexive A R ] (x : A) => *)
-(*   reflexive_partial_app_morphism : Morphism R' (m x). *)
+Section PartialAppTest.
+  Instance and_ar : Params and 0.
+
+  Goal Morphism (iff) (and True True).
+    partial_application_tactic.
+  Admitted.
+
+  Goal Morphism (iff) (or True True).
+    partial_application_tactic.
+    partial_application_tactic. 
+  Admitted.
+
+  Goal Morphism (iff ==> iff) (iff True).
+    partial_application_tactic.
+    (*partial_application_tactic. *)
+   Admitted.
+
+End PartialAppTest.
 
 Hint Extern 4 (@Morphism _ _ _) => partial_application_tactic : typeclass_instances.
 
@@ -395,19 +403,19 @@ Class (A : Type) => Normalizes (m : relation A) (m' : relation A) : Prop :=
   normalizes : relation_equivalence m m'.
 
 Instance inverse_respectful_norm : 
-  Normalizes (A -> B) (inverse R ==> inverse R') (inverse (R ==> R')) .
+  ! Normalizes (A -> B) (inverse R ==> inverse R') (inverse (R ==> R')) .
 Proof. firstorder. Qed.
 
 (* If not an inverse on the left, do a double inverse. *)
 
 Instance not_inverse_respectful_norm : 
-  Normalizes (A -> B) (R ==> inverse R') (inverse (inverse R ==> R')) | 4.
+  ! Normalizes (A -> B) (R ==> inverse R') (inverse (inverse R ==> R')) | 4.
 Proof. firstorder. Qed.
 
 Instance inverse_respectful_rec_norm [ Normalizes B R' (inverse R'') ] :
-  Normalizes (A -> B) (inverse R ==> R') (inverse (R ==> R'')).
-Proof. red ; intros.  
-  pose normalizes as r.
+  ! Normalizes (A -> B) (inverse R ==> R') (inverse (R ==> R'')).
+Proof. red ; intros. 
+  assert(r:=normalizes).
   setoid_rewrite r.
   setoid_rewrite inverse_respectful.
   reflexivity.
@@ -415,8 +423,14 @@ Qed.
 
 (** Once we have normalized, we will apply this instance to simplify the problem. *)
 
-Program Instance morphism_inverse_morphism
-  [ Morphism A R m ] : Morphism (inverse R) m | 2.
+Definition morphism_inverse_morphism [ mor : Morphism A R m ] : Morphism (inverse R) m := mor.
+
+Ltac morphism_inverse :=
+  match goal with
+    [ |- @Morphism _ (flip _) _ ] => eapply @morphism_inverse_morphism
+  end.
+
+Hint Extern 2 (@Morphism _ _ _) => morphism_inverse : typeclass_instances.
 
 (** Bootstrap !!! *)
 
@@ -434,16 +448,16 @@ Qed.
 Lemma morphism_releq_morphism [ Normalizes A R R', Morphism _ R' m ] : Morphism R m.
 Proof.
   intros.
+
   pose respect as r.
   pose normalizes as norm.
   setoid_rewrite norm.
   assumption.
 Qed.
 
-Inductive normalization_done : Prop := did_normalization.
-
 Ltac morphism_normalization := 
   match goal with
+    | [ _ : subrelation_done |- _ ] => fail 1
     | [ _ : normalization_done |- _ ] => fail 1
     | [ |- @Morphism _ _ _ ] => let H := fresh "H" in
       set(H:=did_normalization) ; eapply @morphism_releq_morphism
@@ -464,4 +478,4 @@ Ltac morphism_reflexive :=
     | [ |- @Morphism _ _ _ ] => eapply @reflexive_morphism
   end.
 
-Hint Extern 4 (@Morphism _ _ _) => morphism_reflexive : typeclass_instances.
\ No newline at end of file
+Hint Extern 7 (@Morphism _ _ _) => morphism_reflexive : typeclass_instances.
diff --git a/theories/Classes/Morphisms_Prop.v b/theories/Classes/Morphisms_Prop.v
index 7dc1f95e..ec62e12e 100644
--- a/theories/Classes/Morphisms_Prop.v
+++ b/theories/Classes/Morphisms_Prop.v
@@ -29,7 +29,7 @@ Program Instance not_iff_morphism :
 
 (** Logical conjunction. *)
 
-Program Instance and_impl_iff_morphism :
+Program Instance and_impl_morphism :
   Morphism (impl ==> impl ==> impl) and.
 
 (* Program Instance and_impl_iff_morphism :  *)
@@ -49,7 +49,7 @@ Program Instance and_iff_morphism :
 
 (** Logical disjunction. *)
 
-Program Instance or_impl_iff_morphism : 
+Program Instance or_impl_morphism : 
   Morphism (impl ==> impl ==> impl) or.
 
 (* Program Instance or_impl_iff_morphism :  *)
diff --git a/theories/Classes/Morphisms_Relations.v b/theories/Classes/Morphisms_Relations.v
index 5018fa01..1b389667 100644
--- a/theories/Classes/Morphisms_Relations.v
+++ b/theories/Classes/Morphisms_Relations.v
@@ -48,3 +48,11 @@ Proof. intro. apply (predicate_equivalence_pointwise (cons A (cons A nil))). Qed
 Instance subrelation_pointwise :
   Morphism (subrelation ==> pointwise_relation (A:=A) (pointwise_relation (A:=A) impl)) id.
 Proof. intro. apply (predicate_implication_pointwise (cons A (cons A nil))). Qed.
+
+
+Lemma inverse_pointwise_relation A (R : relation A) : 
+  relation_equivalence (pointwise_relation (inverse R)) (inverse (pointwise_relation (A:=A) R)).
+Proof. intros. split; firstorder. Qed.
+
+
+
diff --git a/theories/Classes/RelationClasses.v b/theories/Classes/RelationClasses.v
index a9a53068..9a43a1ba 100644
--- a/theories/Classes/RelationClasses.v
+++ b/theories/Classes/RelationClasses.v
@@ -1,4 +1,4 @@
-(* -*- coq-prog-args: ("-emacs-U" "-top" "Coq.Classes.RelationClasses") -*- *)
+(* -*- coq-prog-name: "coqtop.byte"; coq-prog-args: ("-emacs-U" "-top" "Coq.Classes.RelationClasses") -*- *)
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
 (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
@@ -14,20 +14,21 @@
    Institution: LRI, CNRS UMR 8623 - UniversitÃcopyright Paris Sud
    91405 Orsay, France *)
 
-(* $Id: RelationClasses.v 11092 2008-06-10 18:28:26Z msozeau $ *)
+(* $Id: RelationClasses.v 11282 2008-07-28 11:51:53Z msozeau $ *)
 
 Require Export Coq.Classes.Init.
 Require Import Coq.Program.Basics.
 Require Import Coq.Program.Tactics.
 Require Export Coq.Relations.Relation_Definitions.
 
+(** We allow to unfold the [relation] definition while doing morphism search. *)
+
+Typeclasses unfold relation.
+
 Notation inverse R := (flip (R:relation _) : relation _).
 
 Definition complement {A} (R : relation A) : relation A := fun x y => R x y -> False.
 
-Definition pointwise_relation {A B : Type} (R : relation B) : relation (A -> B) := 
-  fun f g => forall x : A, R (f x) (g x).
-
 (** These are convertible. *)
 
 Lemma complement_inverse : forall A (R : relation A), complement (inverse R) = inverse (complement R).
@@ -42,7 +43,7 @@ Class Reflexive A (R : relation A) :=
   reflexivity : forall x, R x x.
 
 Class Irreflexive A (R : relation A) := 
-  irreflexivity :> Reflexive A (complement R).
+  irreflexivity :> Reflexive (complement R).
 
 Class Symmetric A (R : relation A) := 
   symmetry : forall x y, R x y -> R y x.
@@ -53,12 +54,6 @@ Class Asymmetric A (R : relation A) :=
 Class Transitive A (R : relation A) := 
   transitivity : forall x y z, R x y -> R y z -> R x z.
 
-Implicit Arguments Reflexive [A].
-Implicit Arguments Irreflexive [A].
-Implicit Arguments Symmetric [A].
-Implicit Arguments Asymmetric [A].
-Implicit Arguments Transitive [A].
-
 Hint Resolve @irreflexivity : ord.
 
 Unset Implicit Arguments.
@@ -91,7 +86,7 @@ Program Instance Reflexive_complement_Irreflexive [ Reflexive A (R : relation A)
     unfold complement.
     red. intros H.
     intros H' ; apply H'.
-    apply (reflexivity H).
+    apply reflexivity.
   Qed.
 
 
@@ -129,7 +124,7 @@ Ltac simpl_relation :=
   unfold flip, impl, arrow ; try reduce ; program_simpl ;
     try ( solve [ intuition ]).
 
-Ltac obligations_tactic ::= simpl_relation.
+Ltac obligation_tactic ::= simpl_relation.
 
 (** Logical implication. *)
 
@@ -171,17 +166,17 @@ Class Equivalence (carrier : Type) (equiv : relation carrier) : Prop :=
 
 (** An Equivalence is a PER plus reflexivity. *)
 
-Instance Equivalence_PER [ Equivalence A R ] : PER A R :=
+Instance Equivalence_PER [ Equivalence A R ] : PER A 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 [ Equivalence A eqA ] => Antisymmetric (R : relation A) := 
+Class Antisymmetric ((equ : Equivalence A eqA)) (R : relation A) := 
   antisymmetry : forall x y, R x y -> R y x -> eqA x y.
 
-Program Instance flip_antiSymmetric [ eq : Equivalence A eqA, ! Antisymmetric eq R ] :
-  Antisymmetric eq (flip R).
+Program Instance flip_antiSymmetric {{Antisymmetric A eqA R}} :
+  ! Antisymmetric A eqA (flip R).
 
 (** Leibinz equality [eq] is an equivalence relation.
    The instance has low priority as it is always applicable 
@@ -372,7 +367,7 @@ Proof. intro A. exact (@predicate_implication_preorder (cons A (cons A nil))). Q
    We give an equivalent definition, up-to an equivalence relation 
    on the carrier. *)
 
-Class [ equ : Equivalence A eqA, PreOrder A R ] => PartialOrder :=
+Class [ equ : Equivalence A eqA, preo : PreOrder A R ] => PartialOrder :=
   partial_order_equivalence : relation_equivalence eqA (relation_conjunction R (inverse R)).
 
 (** The equivalence proof is sufficient for proving that [R] must be a morphism 
@@ -394,7 +389,3 @@ Program Instance subrelation_partial_order :
   Proof.
     unfold relation_equivalence in *. firstorder.
   Qed.
-
-Lemma inverse_pointwise_relation A (R : relation A) : 
-  relation_equivalence (pointwise_relation (inverse R)) (inverse (pointwise_relation (A:=A) R)).
-Proof. reflexivity. Qed.
diff --git a/theories/Classes/SetoidClass.v b/theories/Classes/SetoidClass.v
index a9bdaa8f..178d5333 100644
--- a/theories/Classes/SetoidClass.v
+++ b/theories/Classes/SetoidClass.v
@@ -13,7 +13,7 @@
    Institution: LRI, CNRS UMR 8623 - UniversitĂcopyright Paris Sud
    91405 Orsay, France *)
 
-(* $Id: SetoidClass.v 11065 2008-06-06 22:39:43Z msozeau $ *)
+(* $Id: SetoidClass.v 11282 2008-07-28 11:51:53Z msozeau $ *)
 
 Set Implicit Arguments.
 Unset Strict Implicit.
@@ -41,13 +41,13 @@ Typeclasses unfold equiv.
 (** Shortcuts to make proof search easier. *)
 
 Definition setoid_refl [ sa : Setoid A ] : Reflexive equiv.
-Proof. eauto with typeclass_instances. Qed.
+Proof. typeclasses eauto. Qed.
 
 Definition setoid_sym [ sa : Setoid A ] : Symmetric equiv.
-Proof. eauto with typeclass_instances. Qed.
+Proof. typeclasses eauto. Qed.
 
 Definition setoid_trans [ sa : Setoid A ] : Transitive equiv.
-Proof. eauto with typeclass_instances. Qed.
+Proof. typeclasses eauto. Qed.
 
 Existing Instance setoid_refl.
 Existing Instance setoid_sym.
@@ -123,7 +123,7 @@ Ltac setoidify := repeat setoidify_tac.
 (** Every setoid relation gives rise to a morphism, in fact every partial setoid does. *)
 
 Program Definition setoid_morphism [ sa : Setoid A ] : Morphism (equiv ++> equiv ++> iff) equiv :=
-  trans_sym_morphism.
+  PER_morphism.
 
 (** Add this very useful instance in the database. *)
 
@@ -142,7 +142,7 @@ Program Instance type_equivalence : Equivalence Type type_eq.
 
 Ltac morphism_tac := try red ; unfold arrow ; intros ; program_simpl ; try tauto.
 
-Ltac obligations_tactic ::= morphism_tac.
+Ltac obligation_tactic ::= morphism_tac.
 
 (** These are morphisms used to rewrite at the top level of a proof, 
    using [iff_impl_id_morphism] if the proof is in [Prop] and
@@ -178,4 +178,4 @@ Infix "=~=" := pequiv (at level 70, no associativity) : type_scope.
 
 (** Reset the default Program tactic. *)
 
-Ltac obligations_tactic ::= program_simpl.
+Ltac obligation_tactic ::= program_simpl.
diff --git a/theories/Classes/SetoidDec.v b/theories/Classes/SetoidDec.v
index cf3d202d..8a069343 100644
--- a/theories/Classes/SetoidDec.v
+++ b/theories/Classes/SetoidDec.v
@@ -13,7 +13,7 @@
  * Institution: LRI, CNRS UMR 8623 - UniversitĂcopyright Paris Sud
  *              91405 Orsay, France *)
 
-(* $Id: SetoidDec.v 10919 2008-05-11 22:04:26Z msozeau $ *)
+(* $Id: SetoidDec.v 11282 2008-07-28 11:51:53Z msozeau $ *)
 
 Set Implicit Arguments.
 Unset Strict Implicit.
@@ -27,12 +27,12 @@ Require Export Coq.Classes.SetoidClass.
 
 Require Import Coq.Logic.Decidable.
 
-Class [ Setoid A ] => DecidableSetoid :=
+Class DecidableSetoid A [ Setoid A ] :=
   setoid_decidable : forall x y : A, decidable (x == y).
 
 (** The [EqDec] class gives a decision procedure for a particular setoid equality. *)
 
-Class [ Setoid A ] => EqDec :=
+Class (( s : Setoid A )) => EqDec :=
   equiv_dec : forall x y : A, { x == y } + { x =/= y }.
 
 (** We define the [==] overloaded notation for deciding equality. It does not take precedence
@@ -75,18 +75,18 @@ Require Import Coq.Arith.Arith.
 
 (** The equiv is burried inside the setoid, but we can recover it by specifying which setoid we're talking about. *)
 
-Program Instance eq_setoid : Setoid A :=
+Program Instance eq_setoid A : Setoid A :=
   equiv := eq ; setoid_equiv := eq_equivalence.
 
-Program Instance nat_eq_eqdec : EqDec (@eq_setoid nat) :=
+Program Instance nat_eq_eqdec : EqDec (eq_setoid nat) :=
   equiv_dec := eq_nat_dec.
 
 Require Import Coq.Bool.Bool.
 
-Program Instance bool_eqdec : EqDec (@eq_setoid bool) :=
+Program Instance bool_eqdec : EqDec (eq_setoid bool) :=
   equiv_dec := bool_dec.
 
-Program Instance unit_eqdec : EqDec (@eq_setoid unit) :=
+Program Instance unit_eqdec : EqDec (eq_setoid unit) :=
   equiv_dec x y := in_left.
 
   Next Obligation.
@@ -95,7 +95,7 @@ Program Instance unit_eqdec : EqDec (@eq_setoid unit) :=
     reflexivity.
   Qed.
 
-Program Instance prod_eqdec [ ! EqDec (@eq_setoid A), ! EqDec (@eq_setoid B) ] : EqDec (@eq_setoid (prod A B)) :=
+Program Instance prod_eqdec [ ! EqDec (eq_setoid A), ! EqDec (eq_setoid B) ] : EqDec (eq_setoid (prod A B)) :=
   equiv_dec x y := 
     let '(x1, x2) := x in 
     let '(y1, y2) := y in 
@@ -110,7 +110,7 @@ Program Instance prod_eqdec [ ! EqDec (@eq_setoid A), ! EqDec (@eq_setoid B) ] :
 
 Require Import Coq.Program.FunctionalExtensionality.
 
-Program Instance bool_function_eqdec [ ! EqDec (@eq_setoid A) ] : EqDec (@eq_setoid (bool -> A)) :=
+Program Instance bool_function_eqdec [ ! EqDec (eq_setoid A) ] : EqDec (eq_setoid (bool -> A)) :=
   equiv_dec f g := 
     if f true == g true then
       if f false == g false then in_left
diff --git a/theories/Classes/SetoidTactics.v b/theories/Classes/SetoidTactics.v
index b29a52cc..6398b125 100644
--- a/theories/Classes/SetoidTactics.v
+++ b/theories/Classes/SetoidTactics.v
@@ -13,7 +13,7 @@
  * Institution: LRI, CNRS UMR 8623 - UniversitĂcopyright Paris Sud
  *              91405 Orsay, France *)
 
-(* $Id: SetoidTactics.v 10921 2008-05-12 12:27:25Z msozeau $ *)
+(* $Id: SetoidTactics.v 11282 2008-07-28 11:51:53Z msozeau $ *)
 
 Require Export Coq.Classes.RelationClasses.
 Require Export Coq.Classes.Morphisms.
@@ -24,11 +24,22 @@ Require Export Coq.Relations.Relation_Definitions.
 Set Implicit Arguments.
 Unset Strict Implicit.
 
+(** Setoid relation on a given support: declares a relation as a setoid
+   for use with rewrite. It helps choosing if a rewrite should be handled
+   by setoid_rewrite or the regular rewrite using leibniz equality.
+   Users can declare an [SetoidRelation A RA] anywhere to declare default 
+   relations. This is also done automatically by the [Declare Relation A RA]
+   commands. *)
+
+Class SetoidRelation A (R : relation A).
+
+Instance impl_setoid_relation : SetoidRelation impl.
+Instance iff_setoid_relation : SetoidRelation iff.
+
 (** Default relation on a given support. Can be used by tactics
    to find a sensible default relation on any carrier. Users can 
-   declare an [Instance A RA] anywhere to declare default relations.
-   This is also done by the [Declare Relation A RA] command with no
-   parameters for backward compatibility. *)
+   declare an [Instance def : DefaultRelation A RA] anywhere to 
+   declare default relations. *)
 
 Class DefaultRelation A (R : relation A).
 
@@ -38,7 +49,7 @@ Definition default_relation [ DefaultRelation A R ] := R.
 
 (** Every [Equivalence] gives a default relation, if no other is given (lowest priority). *)
 
-Instance equivalence_default [ Equivalence A R ] : DefaultRelation A R | 4.
+Instance equivalence_default [ Equivalence A R ] : DefaultRelation R | 4.
 
 (** The setoid_replace tactics in Ltac, defined in terms of default relations and
    the setoid_rewrite tactic. *)
@@ -174,3 +185,5 @@ Ltac default_add_morphism_tactic :=
   end.
 
 Ltac add_morphism_tactic := default_add_morphism_tactic.
+
+Ltac obligation_tactic ::= program_simpl.