Syntax changes in typeclasses, remove "?" for usual implicit arguments

binding, add "!" syntax for the new binders which require parameters and
not superclasses. Change backquotes for curly braces for user-given
implicit arguments, following tradition. This requires a hack a la
lpar-id-coloneq. Change ident to global for typeclass names in class
binders. Also requires a similar hack to distinguish between [ C t1 tn ]
and [ c : C t1 tn ]. Update affected theories.

While hacking the parsing of { wf }, factorized the two versions of fix
annotation parsing that were present in g_constr and g_vernac.

Add the possibility of the user optionaly giving the priority for resolve and
exact hints (used by type classes). Syntax not fixed yet: a natural
after the list of lemmas in "Hint Resolve" syntax, a natural after a "|"
after the instance constraint in Instance declarations (ex in
Morphisms.v).


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

7 files changed, 259 insertions, 192 deletions

diff --git a/theories/Classes/Equivalence.v b/theories/Classes/Equivalence.v
index bd525e035..bf2602180 100644
--- a/theories/Classes/Equivalence.v
+++ b/theories/Classes/Equivalence.v
@@ -16,26 +16,27 @@
 
 (* $Id: FSetAVL_prog.v 616 2007-08-08 12:28:10Z msozeau $ *)
 
+Require Export Coq.Program.Basics.
 Require Import Coq.Program.Program.
+
 Require Import Coq.Classes.Init.
+Require Export Coq.Classes.Relations.
+Require Export Coq.Classes.Morphisms.
 
 Set Implicit Arguments.
 Unset Strict Implicit.
 
-Require Export Coq.Classes.Relations.
-Require Export Coq.Classes.Morphisms.
-
 Definition equiv [ Equivalence A R ] : relation A := R.
 
 (** Shortcuts to make proof search possible (unification won't unfold equiv). *)
 
-Definition equivalence_refl [ sa : Equivalence A ] : Reflexive equiv.
+Definition equivalence_refl [ sa : ! Equivalence A ] : Reflexive equiv.
 Proof. eauto with typeclass_instances. Qed.
 
-Definition equivalence_sym [ sa : Equivalence A ] : Symmetric equiv.
+Definition equivalence_sym [ sa : ! Equivalence A ] : Symmetric equiv.
 Proof. eauto with typeclass_instances. Qed.
 
-Definition equivalence_trans [ sa : Equivalence A ] : Transitive equiv.
+Definition equivalence_trans [ sa : ! Equivalence A ] : Transitive equiv.
 Proof. eauto with typeclass_instances. Qed.
 
 (** Overloaded notations for setoid equivalence and inequivalence. Not to be confused with [eq] and [=]. *)
@@ -43,20 +44,22 @@ Proof. eauto with typeclass_instances. Qed.
 (** Subset objects should be first coerced to their underlying type, but that notation doesn't work in the standard case then. *)
 (* Notation " x == y " := (equiv (x :>) (y :>)) (at level 70, no associativity) : type_scope. *)
 
-Notation " x == y " := (equiv x y) (at level 70, no associativity) : type_scope.
+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.
 
-Notation " x =/= y " := (complement equiv x y) (at level 70, no associativity) : type_scope.
+Open Local Scope equiv_scope.
 
 (** Use the [clsubstitute] command which substitutes an equality in every hypothesis. *)
 
 Ltac clsubst H := 
   match type of H with
-    ?x == ?y => clsubstitute H ; clear H x
+    ?x === ?y => clsubstitute H ; clear H x
   end.
 
 Ltac clsubst_nofail :=
   match goal with
-    | [ H : ?x == ?y |- _ ] => clsubst H ; clsubst_nofail
+    | [ H : ?x === ?y |- _ ] => clsubst H ; clsubst_nofail
     | _ => idtac
   end.
   
@@ -64,29 +67,62 @@ Ltac clsubst_nofail :=
 
 Tactic Notation "clsubst" "*" := clsubst_nofail.
 
-Lemma nequiv_equiv_trans : forall [ Equivalence A ] (x y z : A), x =/= y -> y == z -> x =/= z.
+Ltac setoidreplace H t :=
+  let Heq := fresh "Heq" in
+    cut(H) ; [ intro Heq ; setoid_rewrite Heq ; clear Heq | unfold equiv ; t ].
+
+Ltac setoidreplacein H H' t :=
+  let Heq := fresh "Heq" in
+    cut(H) ; [ intro Heq ; setoid_rewrite Heq in H' ; clear Heq | unfold equiv ; t ].
+
+Tactic Notation "setoid_replace" constr(x) "with" constr(y) :=
+  setoidreplace (x === y) idtac.
+
+Tactic Notation "setoid_replace" constr(x) "with" constr(y) "in" hyp(id) :=
+  setoidreplacein (x === y) id idtac.
+
+Tactic Notation "setoid_replace" constr(x) "with" constr(y) "by" tactic(t) :=
+  setoidreplace (x === y) ltac:t.
+
+Tactic Notation "setoid_replace" constr(x) "with" constr(y) "in" hyp(id) "by" tactic(t) :=
+  setoidreplacein (x === y) id ltac:t.
+
+Tactic Notation "setoid_replace" constr(x) "with" constr(y) "using" "relation" constr(rel) :=
+  setoidreplace (rel x y) idtac.
+
+Tactic Notation "setoid_replace" constr(x) "with" constr(y) 
+  "using" "relation" constr(rel) "by" tactic(t) :=
+  setoidreplace (rel x y) ltac:t.
+
+Tactic Notation "setoid_replace" constr(x) "with" constr(y) "in" hyp(id) 
+  "using" "relation" constr(rel) :=
+  setoidreplacein (rel x y) id idtac.
+
+Tactic Notation "setoid_replace" constr(x) "with" constr(y) "in" hyp(id)
+  "using" "relation" constr(rel) "by" tactic(t) :=
+  setoidreplacein (rel x y) id ltac:t.
+  
+Lemma nequiv_equiv_trans : forall [ ! Equivalence A ] (x y z : A), x =/= y -> y === z -> x =/= z.
 Proof with auto.
   intros; intro.
-  assert(z == y) by relation_sym.
-  assert(x == y) by relation_trans.
+  assert(z === y) by relation_sym.
+  assert(x === y) by relation_trans.
   contradiction.
 Qed.
 
-Lemma equiv_nequiv_trans : forall [ Equivalence A ] (x y z : A), x == y -> y =/= z -> x =/= z.
+Lemma equiv_nequiv_trans : forall [ ! Equivalence A ] (x y z : A), x === y -> y =/= z -> x =/= z.
 Proof.
   intros; intro. 
-  assert(y == x) by relation_sym.
-  assert(y == z) by relation_trans.
+  assert(y === x) by relation_sym.
+  assert(y === z) by relation_trans.
   contradiction.
 Qed.
 
-Open Scope type_scope.
-
 Ltac equiv_simplify_one :=
   match goal with
-    | [ H : ?x == ?x |- _ ] => clear H
-    | [ H : ?x == ?y |- _ ] => clsubst H
-    | [ |- ?x =/= ?y ] => let name:=fresh "Hneq" in intro name
+    | [ H : (?x === ?x)%type |- _ ] => clear H
+    | [ H : (?x === ?y)%type |- _ ] => clsubst H
+    | [ |- (?x =/= ?y)%type ] => let name:=fresh "Hneq" in intro name
   end.
 
 Ltac equiv_simplify := repeat equiv_simplify_one.
@@ -101,13 +137,13 @@ Ltac equivify := repeat equivify_tac.
 
 (** Every equivalence relation gives rise to a morphism, as it is transitive and symmetric. *)
 
-Instance [ sa : Equivalence A ] => equiv_morphism : ? Morphism (equiv ++> equiv ++> iff) equiv :=
+Instance [ sa : ! Equivalence ] => equiv_morphism : Morphism (equiv ++> equiv ++> iff) equiv :=
   respect := respect.
 
 (** The partial application too as it is reflexive. *)
 
-Instance [ sa : Equivalence A ] (x : A) => 
-  equiv_partial_app_morphism : ? Morphism (equiv ++> iff) (equiv x) :=
+Instance [ sa : ! Equivalence A ] (x : A) => 
+  equiv_partial_app_morphism : Morphism (equiv ++> iff) (equiv x) :=
   respect := respect. 
 
 Definition type_eq : relation Type :=
@@ -125,24 +161,11 @@ Ltac obligations_tactic ::= morphism_tac.
    using [iff_impl_id_morphism] if the proof is in [Prop] and
    [eq_arrow_id_morphism] if it is in Type. *)
 
-Program Instance iff_impl_id_morphism : ? Morphism (iff ++> impl) id.
+Program Instance iff_impl_id_morphism : 
+  Morphism (iff ++> impl) id.
 
 (* Program Instance eq_arrow_id_morphism : ? Morphism (eq +++> arrow) id. *)
 
-(* Definition compose_respect (A B C : Type) (R : relation (A -> B)) (R' : relation (B -> C)) *)
-(*   (x y : A -> C) : Prop := forall (f : A -> B) (g : B -> C), R f f -> R' g g. *)
-
-(* Program Instance (A B C : Type) (R : relation (A -> B)) (R' : relation (B -> C)) *)
-(*   [ mg : ? Morphism R' g ] [ mf : ? Morphism R f ] =>  *)
-(*   compose_morphism : ? Morphism (compose_respect R R') (g o f). *)
-
-(* Next Obligation. *)
-(* Proof. *)
-(*   apply (respect (m0:=mg)). *)
-(*   apply (respect (m0:=mf)). *)
-(*   assumption. *)
-(* Qed. *)
-
 (** Partial equivs don't require reflexivity so we can build a partial equiv on the function space. *)
 
 Class PartialEquivalence (carrier : Type) (pequiv : relation carrier) :=
@@ -155,3 +178,14 @@ Class PartialEquivalence (carrier : Type) (pequiv : relation carrier) :=
 (** Reset the default Program tactic. *)
 
 Ltac obligations_tactic ::= program_simpl.
+
+(** Default relation on a given support. *)
+
+Class DefaultRelation A := default_relation : relation A.
+
+(** Every [Equivalence] gives a default relation, if no other is given (lowest priority). *)
+
+Instance [ ! Equivalence A R ] => 
+  equivalence_default : DefaultRelation A | 4 := 
+  default_relation := R.
+
diff --git a/theories/Classes/Functions.v b/theories/Classes/Functions.v
index 7942d3642..c08dee76f 100644
--- a/theories/Classes/Functions.v
+++ b/theories/Classes/Functions.v
@@ -22,22 +22,22 @@ Require Export Coq.Classes.Morphisms.
 Set Implicit Arguments.
 Unset Strict Implicit.
 
-Class [ m : Morphism (A -> B) (RA ++> RB) f ] => Injective :=
+Class [ m : ! Morphism (A -> B) (RA ++> RB) f ] => Injective :=
   injective : forall x y : A, RB (f x) (f y) -> RA x y.
 
-Class [ m : Morphism (A -> B) (RA ++> RB) f ] => Surjective :=
+Class [ m : ! Morphism (A -> B) (RA ++> RB) f ] => Surjective :=
   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 [ m : ! Morphism (A -> B) (eqA ++> eqB) ] => MonoMorphism :=
   monic :> Injective m.
 
-Class [ m : Morphism (A -> B) (eqA ++> eqB) ] => EpiMorphism :=
+Class [ m : ! Morphism (A -> B) (eqA ++> eqB) ] => EpiMorphism :=
   epic :> Surjective m.
 
-Class [ m : Morphism (A -> B) (eqA ++> eqB) ] => IsoMorphism :=
+Class [ m : ! Morphism (A -> B) (eqA ++> eqB) ] => IsoMorphism :=
   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/Morphisms.v b/theories/Classes/Morphisms.v
index 5d679d2c9..fb0acb39c 100644
--- a/theories/Classes/Morphisms.v
+++ b/theories/Classes/Morphisms.v
@@ -10,7 +10,7 @@
 (* Typeclass-based morphisms with standard instances for equivalence relations.
  
    Author: Matthieu Sozeau
-   Institution: LRI, CNRS UMR 8623 - UniversitĂcopyright Paris Sud
+   Institution: LRI, CNRS UMR 8623 - UniversitÃcopyright Paris Sud
    91405 Orsay, France *)
 
 (* $Id: FSetAVL_prog.v 616 2007-08-08 12:28:10Z msozeau $ *)
@@ -37,8 +37,8 @@ Definition respectful A (R : relation A) B (R' : relation B) : relation (A -> B)
 
 (** Notations reminiscent of the old syntax for declaring morphisms. *)
 
-Notation " R ==> R' " := (@respectful _ R _ R') (right associativity, at level 20).
 Notation " R ++> R' " := (@respectful _ R _ R') (right associativity, at level 20).
+Notation " R ==> R' " := (@respectful _ R _ R') (right associativity, at level 20).
 Notation " R --> R' " := (@respectful _ (inverse R) _ R') (right associativity, at level 20).
 
 (** A morphism on a relation [R] is an object respecting the relation (in its kernel). 
@@ -106,34 +106,87 @@ Qed.
 
 (* Program Definition arrow_morphism `A B` (m : A -> B) : Morphism (eq ++> eq) m. *)
 
-(** Any binary morphism respecting some relations up to [iff] respects 
+(** Any morphism respecting some relations up to [iff] respects 
    them up to [impl] in each way. Very important instances as we need [impl]
    morphisms at the top level when we rewrite. *)
 
-Program Instance `A` (R : relation A) `B` (R' : relation B)
-  [ ? Morphism (R ++> R' ++> iff) m ] =>
+Class SubRelation A (R S : relation A) :=
+  subrelation :> Morphism (S ==> R) (fun x => x).
 
-  iff_impl_binary_morphism : ? Morphism (R ++> R' ++> impl) m.
+Instance iff_impl_subrelation : SubRelation Prop impl iff.
+Proof.
+  constructor ; red ; intros.
+  tauto.
+Qed.
 
-  Next Obligation.
-  Proof.
-    destruct respect with x y x0 y0 ; auto.
-  Qed.
+Instance iff_inverse_impl_subrelation : SubRelation Prop (inverse impl) iff.
+Proof.
+  constructor ; red ; intros.
+  tauto.
+Qed.
 
-Program Instance (A : Type) (R : relation A) `B` (R' : relation B)
-  [ ? Morphism (R ++> R' ++> iff) m ] =>
-  iff_inverse_impl_binary_morphism : ? Morphism (R ++> R' ++> inverse impl) m.
+Instance [ SubRelation A R₁ R₂ ] =>
+  morphisms_subrelation : SubRelation (B -> A) (R ==> R₁) (R ==> R₂).
+Proof.
+  constructor ; repeat red ; intros.
+  destruct subrelation.
+  red in respect0, H ; unfold id in *.
+  apply respect0.
+  apply H.
+  apply H0.
+Qed.
 
-  Next Obligation.
-  Proof.
-    destruct respect with x y x0 y0 ; auto.
-  Qed.
+(** High priority because it is always applicable and loops. *)
+
+Instance [ SubRelation A R₁ R₂, Morphism R₂ m ] =>
+  subrelation_morphism : Morphism R₁ m | 4.
+Proof.
+  destruct subrelation.
+  red in respect0.
+  unfold id in * ; apply respect0.
+  apply respect.
+Qed.
+
+(* Program Instance `A` (R : relation A) `B` (R' : relation B) *)
+(*   [ ? Morphism (R ==> R' ==> iff) m ] => *)
+(*   iff_impl_binary_morphism : ? Morphism (R ==> R' ==> impl) m. *)
+
+(*   Next Obligation. *)
+(*   Proof. *)
+(*     destruct respect with x y x0 y0 ; auto. *)
+(*   Qed. *)
+
+(* Program Instance `A` (R : relation A) `B` (R' : relation B) *)
+(*   [ ? Morphism (R ==> R' ==> iff) m ] => *)
+(*   iff_inverse_impl_binary_morphism : ? Morphism (R ==> R' ==> inverse impl) m. *)
+
+(*   Next Obligation. *)
+(*   Proof. *)
+(*     destruct respect with x y x0 y0 ; auto. *)
+(*   Qed. *)
+
+
+(* Program Instance [ Morphism (A -> Prop) (R ==> iff) m ] => *)
+(*   iff_impl_morphism : ? Morphism (R ==> impl) m. *)
+
+(*   Next Obligation. *)
+(*   Proof. *)
+(*     destruct respect with x y ; auto. *)
+(*   Qed. *)
+
+(* Program Instance [ Morphism (A -> Prop) (R ==> iff) m ] => *)
+(*   iff_inverse_impl_morphism : ? Morphism (R ==> inverse impl) m. *)
+
+(*   Next Obligation. *)
+(*   Proof. *)
+(*     destruct respect with x y ; auto. *)
+(*   Qed. *)
 
 (** Logical implication [impl] is a morphism for logical equivalence. *)
 
-Program Instance iff_iff_iff_impl_morphism : ? Morphism (iff ++> iff ++> iff) impl.
+Program Instance iff_iff_iff_impl_morphism : Morphism (iff ==> iff ==> iff) impl.
 
-Lemma reflexive_impl_iff [ Symmetric A R, ? Morphism (R ++> impl) m ] : Morphism (R ==> iff) m.
+Lemma reflexive_impl_iff [ ! Symmetric A R, Morphism (R ==> impl) m ] : Morphism (R ==> iff) m.
 Proof.
   intros.
   constructor. red ; intros. 
@@ -142,8 +195,8 @@ Qed.
 
 (** The complement of a relation conserves its morphisms. *)
 
-Program Instance `A` (RA : relation A) [ ? Morphism (RA ++> RA ++> iff) R ] => 
-  complement_morphism : ? Morphism (RA ++> RA ++> iff) (complement R).
+Program Instance {A} (RA : relation A) [ Morphism (RA ==> RA ==> iff) R ] => 
+  complement_morphism : Morphism (RA ==> RA ==> iff) (complement R).
 
   Next Obligation.
   Proof.
@@ -156,8 +209,8 @@ Program Instance `A` (RA : relation A) [ ? Morphism (RA ++> RA ++> iff) R ] =>
 
 (** The inverse too. *)
 
-Program Instance `A` (RA : relation A) [ ? Morphism (RA ++> RA ++> iff) R ] => 
-  inverse_morphism : ? Morphism (RA ++> RA ++> iff) (inverse R).
+Program Instance {A} (RA : relation A) [ Morphism (RA ==> RA ==> iff) R ] => 
+  inverse_morphism : Morphism (RA ==> RA ==> iff) (inverse R).
 
   Next Obligation.
   Proof.
@@ -165,8 +218,8 @@ Program Instance `A` (RA : relation A) [ ? Morphism (RA ++> RA ++> iff) R ] =>
     apply respect ; auto.
   Qed.
 
-Program Instance (A B C : Type) [ ? Morphism (RA ++> RB ++> RC) (f : A -> B -> C) ] => 
-  flip_morphism : ? Morphism (RB ++> RA ++> RC) (flip f).
+Program Instance {A B C : Type} [ Morphism (RA ==> RB ==> RC) (f : A -> B -> C) ] => 
+  flip_morphism : Morphism (RB ==> RA ==> RC) (flip f).
 
   Next Obligation.
   Proof.
@@ -174,51 +227,13 @@ Program Instance (A B C : Type) [ ? Morphism (RA ++> RB ++> RC) (f : A -> B -> C
     apply respect ; auto.
   Qed.
 
-(* Definition respectful' A (R : relation A) B (R' : relation B) (f : A -> B) : relation A := *)
-(*   fun x y => R x y -> R' (f x) (f y). *)
-
-(* Definition morphism_respectful' A R B (R' : relation B) (f : A -> B) *)
-(*   [ ? Morphism (R ++> R') f ] (x y : A) : respectful' R R' f x y. *)
-(* intros. *)
-(* destruct H. *)
-(* red in respect0. *)
-(* red.  *)
-(* apply respect0. *)
-(* Qed. *)
-
-(* Existing Instance morphism_respectful'. *)
-
-(* Goal forall A [ Equivalence A (eqA : relation A) ] R [ ? Morphism (eqA ++> iff) m ] (x y : A)  *)
-(*   [ ? Morphism (eqA ++> eqA) m' ] (m' : A -> A), eqA x y -> True. *)
-(*   intros. *)
-(*   cut (relation A) ; intros R'. *)
-(*   cut ((eqA ++> R') m' m') ; intros. *)
-(*   assert({ R' : relation A & Reflexive R' }). *)
-(*   econstructor. *)
-(*   typeclass_instantiation. *)
-  
-
-(*   assert (exists R' : relation A, Morphism ((fun x y => eqA x y -> R' (m' x) (m' y)) ++> iff) m). *)
-(*   eapply ex_intro. *)
-(*   unfold respectful. *)
-(*   typeclass_instantiation. *)
-  
-
-(*   assert (exists R', Morphism (R' ++> iff) m /\ Morphism (eqA ++> R') m'). *)
-(*   typeclass_instantiation. *)
-(*   Set Printing All. *)
-(*   Show Proof. *)
-  
-  
-(*   apply respect. *)
-
 (** Partial applications are ok when a proof of refl is available. *)
 
 (** A proof of [R x x] is available. *)
 
 (* Program Instance (A : Type) R B (R' : relation B) *)
-(*   [ ? Morphism (R ++> R') m ] [ ? Morphism R x ] => *)
-(*   morphism_partial_app_morphism : ? Morphism R' (m x). *)
+(*   [ Morphism (R ==> R') m ] [ Morphism R x ] => *)
+(*   morphism_partial_app_morphism : Morphism R' (m x). *)
 
 (*   Next Obligation. *)
 (*   Proof with auto. *)
@@ -229,24 +244,24 @@ Program Instance (A B C : Type) [ ? Morphism (RA ++> RB ++> RC) (f : A -> B -> C
 
 (** Morpshism declarations for partial applications. *)
 
-Program Instance [ Transitive A R ] (x : A) =>
-  trans_contra_inv_impl_morphism : ? Morphism (R --> inverse impl) (R x).
+Program Instance [ ! Transitive A R ] (x : A) =>
+  trans_contra_inv_impl_morphism : Morphism (R --> inverse impl) (R x).
 
   Next Obligation.
   Proof with auto.
     trans y...
   Qed.
 
-Program Instance [ Transitive A R ] (x : A) =>
-  trans_co_impl_morphism : ? Morphism (R ++> impl) (R x).
+Program Instance [ ! Transitive A R ] (x : A) =>
+  trans_co_impl_morphism : Morphism (R ==> impl) (R x).
 
   Next Obligation.
   Proof with auto.
     trans x0...
   Qed.
 
-Program Instance [ Transitive A R, Symmetric A R ] (x : A) =>
-  trans_sym_co_inv_impl_morphism : ? Morphism (R ++> inverse impl) (R x).
+Program Instance [ ! Transitive A R, Symmetric R ] (x : A) =>
+  trans_sym_co_inv_impl_morphism : Morphism (R ==> inverse impl) (R x).
 
   Next Obligation.
   Proof with auto.
@@ -254,8 +269,8 @@ Program Instance [ Transitive A R, Symmetric A R ] (x : A) =>
     sym...
   Qed.
 
-Program Instance [ Transitive A R, Symmetric A R ] (x : A) =>
-  trans_sym_contra_impl_morphism : ? Morphism (R --> impl) (R x).
+Program Instance [ ! Transitive A R, Symmetric R ] (x : A) =>
+  trans_sym_contra_impl_morphism : Morphism (R --> impl) (R x).
 
   Next Obligation.
   Proof with auto.
@@ -264,7 +279,7 @@ Program Instance [ Transitive A R, Symmetric A R ] (x : A) =>
   Qed.
 
 Program Instance [ Equivalence A R ] (x : A) =>
-  equivalence_partial_app_morphism : ? Morphism (R ++> iff) (R x).
+  equivalence_partial_app_morphism : Morphism (R ==> iff) (R x).
 
   Next Obligation.
   Proof with auto.
@@ -277,8 +292,8 @@ Program Instance [ Equivalence A R ] (x : A) =>
 (** With symmetric relations, variance is no issue ! *)
 
 (* Program Instance (A B : Type) (R : relation A) (R' : relation B) *)
-(*   [ Morphism _ (R ++> R') m ] [ Symmetric A R ] =>  *)
-(*   sym_contra_morphism : ? Morphism (R --> R') m. *)
+(*   [ Morphism _ (R ==> R') m ] [ Symmetric A R ] =>  *)
+(*   sym_contra_morphism : Morphism (R --> R') m. *)
 
 (*   Next Obligation. *)
 (*   Proof with auto. *)
@@ -289,8 +304,8 @@ Program Instance [ Equivalence A R ] (x : A) =>
 (** [R] is reflexive, hence we can build the needed proof. *)
 
 Program Instance (A B : Type) (R : relation A) (R' : relation B)
-  [ ? Morphism (R ++> R') m ] [ Reflexive A R ] (x : A) =>
-  reflexive_partial_app_morphism : ? Morphism R' (m x).
+  [ Morphism (R ==> R') m ] [ Reflexive R ] (x : A) =>
+  reflexive_partial_app_morphism : Morphism R' (m x) | 3.
 
   Next Obligation.
   Proof with auto.
@@ -302,8 +317,8 @@ Program Instance (A B : Type) (R : relation A) (R' : relation B)
 (** 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 [ Transitive A R ] => 
-  trans_co_eq_inv_impl_morphism : ? Morphism (R ++> eq ++> inverse impl) R.
+Program Instance [ ! Transitive A R ] => 
+  trans_co_eq_inv_impl_morphism : Morphism (R ==> eq ==> inverse impl) R.
 
   Next Obligation.
   Proof with auto.
@@ -311,8 +326,8 @@ Program Instance [ Transitive A R ] =>
     subst x0...
   Qed.
 
-Program Instance [ Transitive A R ] => 
-  trans_contra_eq_inv_impl_morphism : ? Morphism (R --> eq ++> impl) R.
+Program Instance [ ! Transitive A R ] => 
+  trans_contra_eq_impl_morphism : Morphism (R --> eq ==> impl) R.
 
   Next Obligation.
   Proof with auto.
@@ -322,8 +337,8 @@ Program Instance [ Transitive A R ] =>
 
 (** Every symmetric and transitive relation gives rise to an equivariant morphism. *)
 
-Program Instance [ Transitive A R, Symmetric A R ] => 
-  trans_sym_morphism : ? Morphism (R ++> R ++> iff) R.
+Program Instance [ ! Transitive A R, Symmetric R ] => 
+  trans_sym_morphism : Morphism (R ==> R ==> iff) R.
 
   Next Obligation.
   Proof with auto.
@@ -334,7 +349,7 @@ Program Instance [ Transitive A R, Symmetric A R ] =>
   Qed.
 
 Program Instance [ Equivalence A R ] => 
-  equiv_morphism : ? Morphism (R ++> R ++> iff) R.
+  equiv_morphism : Morphism (R ==> R ==> iff) R.
 
   Next Obligation.
   Proof with auto.
@@ -346,44 +361,65 @@ Program Instance [ Equivalence A R ] =>
 
 (** In case the rewrite happens at top level. *)
 
-Program Instance iff_inverse_impl_id : 
-  ? Morphism (iff ++> inverse impl) id.
+Program Instance iff_inverse_impl_id :
+  Morphism (iff ==> inverse impl) id.
 
-Program Instance inverse_iff_inverse_impl_id : 
-  ? Morphism (iff --> inverse impl) id.
+Program Instance inverse_iff_inverse_impl_id :
+  Morphism (iff --> inverse impl) id.
   
-Program Instance iff_impl_id : 
-  ? Morphism (iff ++> impl) id.
+Program Instance iff_impl_id :
+  Morphism (iff ==> impl) id.
 
-Program Instance inverse_iff_impl_id : 
-  ? Morphism (iff --> impl) id.
+Program Instance inverse_iff_impl_id :
+  Morphism (iff --> impl) id.
   
 (** Standard instances for [iff] and [impl]. *)
 
 (** Logical conjunction. *)
 
-Program Instance and_impl_iff_morphism : ? Morphism (impl ++> iff ++> impl) and.
+Program Instance and_impl_iff_morphism : 
+  Morphism (impl ==> iff ==> impl) and.
 
-Program Instance and_iff_impl_morphism : ? Morphism (iff ++> impl ++> impl) and.
+Program Instance and_iff_impl_morphism : 
+  Morphism (iff ==> impl ==> impl) and.
 
 Program Instance and_inverse_impl_iff_morphism : 
-  ? Morphism (inverse impl ++> iff ++> inverse impl) and.
+  Morphism (inverse impl ==> iff ==> inverse impl) and.
 
 Program Instance and_iff_inverse_impl_morphism : 
-  ? Morphism (iff ++> inverse impl ++> inverse impl) and.
+  Morphism (iff ==> inverse impl ==> inverse impl) and.
 
-Program Instance and_iff_morphism : ? Morphism (iff ++> iff ++> iff) and.
+Program Instance and_iff_morphism : 
+  Morphism (iff ==> iff ==> iff) and.
 
 (** Logical disjunction. *)
 
-Program Instance or_impl_iff_morphism : ? Morphism (impl ++> iff ++> impl) or.
+Program Instance or_impl_iff_morphism : 
+  Morphism (impl ==> iff ==> impl) or.
 
-Program Instance or_iff_impl_morphism : ? Morphism (iff ++> impl ++> impl) or.
+Program Instance or_iff_impl_morphism : 
+  Morphism (iff ==> impl ==> impl) or.
 
 Program Instance or_inverse_impl_iff_morphism :
-  ? Morphism (inverse impl ++> iff ++> inverse impl) or.
+  Morphism (inverse impl ==> iff ==> inverse impl) or.
 
 Program Instance or_iff_inverse_impl_morphism : 
-  ? Morphism (iff ++> inverse impl ++> inverse impl) or.
+  Morphism (iff ==> inverse impl ==> inverse impl) or.
+
+Program Instance or_iff_morphism : 
+  Morphism (iff ==> iff ==> iff) or.
 
-Program Instance or_iff_morphism : ? Morphism (iff ++> iff ++> iff) or.
+(** Coq functions are morphisms for leibniz equality, 
+   applied only if really needed. *)
+
+Instance {A B : Type} (m : A -> B) =>
+  any_eq_eq_morphism : Morphism (@Logic.eq A ==> @Logic.eq B) m | 4.
+Proof.
+  red ; intros. subst ; reflexivity.
+Qed.
+
+Instance {A : Type} (m : A -> Prop) =>
+  any_eq_iff_morphism : Morphism (@Logic.eq A ==> iff) m | 4.
+Proof.
+  red ; intros. subst ; reflexivity.
+Qed.
diff --git a/theories/Classes/Relations.v b/theories/Classes/Relations.v
index 28f582c3d..b14647d06 100644
--- a/theories/Classes/Relations.v
+++ b/theories/Classes/Relations.v
@@ -63,46 +63,46 @@ Hint Resolve @irreflexive : ord.
 
 (** We can already dualize all these properties. *)
 
-Program Instance [ Reflexive A R ] => flip_reflexive : Reflexive A (flip R) :=
+Program Instance [ bla : ! Reflexive A R ] => flip_reflexive : Reflexive (flip R) :=
   reflexive := reflexive (R:=R).
 
-Program Instance [ Irreflexive A R ] => flip_irreflexive : Irreflexive A (flip R) :=
+Program Instance [ ! Irreflexive A R ] => flip_irreflexive : Irreflexive (flip R) :=
   irreflexive := irreflexive (R:=R).
 
-Program Instance [ Symmetric A R ] => flip_symmetric : Symmetric A (flip R).
+Program Instance [ ! Symmetric A R ] => flip_symmetric : Symmetric (flip R).
 
   Solve Obligations using unfold flip ; program_simpl ; clapply symmetric.
 
-Program Instance [ Asymmetric A R ] => flip_asymmetric : Asymmetric A (flip R).
+Program Instance [ ! Asymmetric A R ] => flip_asymmetric : Asymmetric (flip R).
   
   Solve Obligations using program_simpl ; unfold flip in * ; intros ; clapply asymmetric.
 
-Program Instance [ Transitive A R ] => flip_transitive : Transitive A (flip R).
+Program Instance [ ! Transitive A R ] => flip_transitive : Transitive (flip R).
 
   Solve Obligations using unfold flip ; program_simpl ; clapply transitive.
 
 (** Have to do it again for Prop. *)
 
-Program Instance [ Reflexive A (R : relation A) ] => inverse_reflexive : Reflexive A (inverse R) :=
+Program Instance [ ! Reflexive A (R : relation A) ] => inverse_reflexive : Reflexive (inverse R) :=
   reflexive := reflexive (R:=R).
 
-Program Instance [ Irreflexive A (R : relation A) ] => inverse_irreflexive : Irreflexive A (inverse R) :=
+Program Instance [ ! Irreflexive A (R : relation A) ] => inverse_irreflexive : Irreflexive (inverse R) :=
   irreflexive := irreflexive (R:=R).
 
-Program Instance [ Symmetric A (R : relation A) ] => inverse_symmetric : Symmetric A (inverse R).
+Program Instance [ ! Symmetric A (R : relation A) ] => inverse_symmetric : Symmetric (inverse R).
 
   Solve Obligations using unfold inverse, flip ; program_simpl ; clapply symmetric.
 
-Program Instance [ Asymmetric A (R : relation A) ] => inverse_asymmetric : Asymmetric A (inverse R).
+Program Instance [ ! Asymmetric A (R : relation A) ] => inverse_asymmetric : Asymmetric (inverse R).
   
   Solve Obligations using program_simpl ; unfold inverse, flip in * ; intros ; clapply asymmetric.
 
-Program Instance [ Transitive A (R : relation A) ] => inverse_transitive : Transitive A (inverse R).
+Program Instance [ ! Transitive A (R : relation A) ] => inverse_transitive : Transitive (inverse R).
 
   Solve Obligations using unfold inverse, flip ; program_simpl ; clapply transitive.
 
-Program Instance [ Reflexive A (R : relation A) ] => 
-  reflexive_complement_irreflexive : Irreflexive A (complement R).
+Program Instance [ ! Reflexive A (R : relation A) ] => 
+  reflexive_complement_irreflexive : Irreflexive (complement R).
 
   Next Obligation. 
   Proof. 
@@ -110,8 +110,8 @@ Program Instance [ Reflexive A (R : relation A) ] =>
     apply reflexive.
   Qed.
 
-Program Instance [ Irreflexive A (R : relation A) ] => 
-  irreflexive_complement_reflexive : Reflexive A (complement R).
+Program Instance [ ! Irreflexive A (R : relation A) ] => 
+  irreflexive_complement_reflexive : Reflexive (complement R).
 
   Next Obligation. 
   Proof. 
@@ -119,7 +119,7 @@ Program Instance [ Irreflexive A (R : relation A) ] =>
     apply (irreflexive H).
   Qed.
 
-Program Instance [ Symmetric A (R : relation A) ] => complement_symmetric : Symmetric A (complement R).
+Program Instance [ ! Symmetric A (R : relation A) ] => complement_symmetric : Symmetric (complement R).
 
   Next Obligation.
   Proof.
@@ -137,20 +137,20 @@ Ltac obligations_tactic ::= simpl_relation.
 
 (** Logical implication. *)
 
-Program Instance impl_refl : ? Reflexive impl.
-Program Instance impl_trans : ? Transitive impl.
+Program Instance impl_refl : Reflexive impl.
+Program Instance impl_trans : Transitive impl.
 
 (** Logical equivalence. *)
 
-Program Instance iff_refl : ? Reflexive iff.
-Program Instance iff_sym : ? Symmetric iff.
-Program Instance iff_trans : ? Transitive iff.
+Program Instance iff_refl : Reflexive iff.
+Program Instance iff_sym : Symmetric iff.
+Program Instance iff_trans : Transitive iff.
 
 (** Leibniz equality. *)
 
-Program Instance eq_refl : ? Reflexive (@eq A).
-Program Instance eq_sym : ? Symmetric (@eq A).
-Program Instance eq_trans : ? Transitive (@eq A).
+Program Instance eq_refl : Reflexive (@eq A).
+Program Instance eq_sym : Symmetric (@eq A).
+Program Instance eq_trans : Transitive (@eq A).
 
 (** ** General tactics to solve goals on relations.
    Each tactic comes in two flavors:
@@ -298,9 +298,7 @@ Class PreOrder A (R : relation A) :=
   preorder_refl :> Reflexive R ;
   preorder_trans :> Transitive R.
 
-(** A [PreOrder] is both reflexive and transitive. *)
-
-(** The [PER] typeclass. *)
+(** A partial equivalence relation is symmetric and transitive. *)
 
 Class PER (carrier : Type) (pequiv : relation carrier) :=
   per_sym :> Symmetric pequiv ;
@@ -332,13 +330,13 @@ Class Equivalence (carrier : Type) (equiv : relation carrier) :=
 Class [ Equivalence A eqA ] => Antisymmetric (R : relation A) := 
   antisymmetric : forall x y, R x y -> R y x -> eqA x y.
 
-Program Instance [ eq : Equivalence A eqA, ? Antisymmetric eq R ] => 
-  flip_antisymmetric : ? Antisymmetric eq (flip R).
+Program Instance [ eq : Equivalence A eqA, Antisymmetric eq R ] => 
+  flip_antisymmetric : Antisymmetric eq (flip R).
 
   Solve Obligations using unfold inverse, flip ; program_simpl ; eapply @antisymmetric ; eauto.
 
-Program Instance [ eq : Equivalence A eqA, ? Antisymmetric eq (R : relation A) ] => 
-  inverse_antisymmetric : ? Antisymmetric eq (inverse R).
+Program Instance [ eq : Equivalence A eqA, Antisymmetric eq (R : relation A) ] => 
+  inverse_antisymmetric : Antisymmetric eq (inverse R).
 
   Solve Obligations using unfold inverse, flip ; program_simpl ; eapply @antisymmetric ; eauto.
 
diff --git a/theories/Classes/SetoidClass.v b/theories/Classes/SetoidClass.v
index 571f65b62..9dd4f6181 100644
--- a/theories/Classes/SetoidClass.v
+++ b/theories/Classes/SetoidClass.v
@@ -149,7 +149,7 @@ Ltac obligations_tactic ::= morphism_tac.
    using [iff_impl_id_morphism] if the proof is in [Prop] and
    [eq_arrow_id_morphism] if it is in Type. *)
 
-Program Instance iff_impl_id_morphism : ? Morphism (iff ++> impl) id.
+Program Instance iff_impl_id_morphism : Morphism (iff ++> impl) id.
 
 (* Program Instance eq_arrow_id_morphism : ? Morphism (eq +++> arrow) id. *)
 
diff --git a/theories/Classes/SetoidDec.v b/theories/Classes/SetoidDec.v
index c385fc5b5..8a435b449 100644
--- a/theories/Classes/SetoidDec.v
+++ b/theories/Classes/SetoidDec.v
@@ -42,7 +42,7 @@ Notation " x == y " := (equiv_dec (x :>) (y :>)) (no associativity, at level 70)
 
 (** Use program to solve some obligations. *)
 
-Definition swap_sumbool `A B` (x : { A } + { B }) : { B } + { A } :=
+Definition swap_sumbool {A B} (x : { A } + { B }) : { B } + { A } :=
   match x with
     | left H => @right _ _ H 
     | right H => @left _ _ H 
@@ -52,7 +52,7 @@ Require Import Coq.Program.Program.
 
 (** 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. *)
 
@@ -60,10 +60,10 @@ Infix "=/=" := nequiv_dec (no associativity, at level 70).
 
 (** Define boolean versions, losing the logical information. *)
 
-Definition equiv_decb [ EqDec A ] (x y : A) : bool :=
+Definition equiv_decb [ ! EqDec A ] (x y : A) : bool :=
   if x == y then true else false.
 
-Definition nequiv_decb [ EqDec A ] (x y : A) : bool :=
+Definition nequiv_decb [ ! EqDec A ] (x y : A) : bool :=
   negb (equiv_decb x y).
 
 Infix "==b" := equiv_decb (no associativity, at level 70).
@@ -78,15 +78,15 @@ Require Import Coq.Arith.Arith.
 Program Instance eq_setoid : 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 := left.
 
   Next Obligation.
@@ -95,8 +95,8 @@ Program Instance unit_eqdec : ? EqDec (@eq_setoid unit) :=
     reflexivity.
   Qed.
 
-Program Instance [ ? EqDec (@eq_setoid A), ? EqDec (@eq_setoid B) ] => 
-  prod_eqdec : ? EqDec (@eq_setoid (prod A B)) :=
+Program Instance [ EqDec (@eq_setoid A), EqDec (@eq_setoid B) ] => 
+  prod_eqdec : EqDec (@eq_setoid (prod A B)) :=
   equiv_dec x y := 
     dest x as (x1, x2) in 
     dest y as (y1, y2) in 
@@ -111,7 +111,7 @@ Program Instance [ ? EqDec (@eq_setoid A), ? EqDec (@eq_setoid B) ] =>
 
 Require Import Coq.Program.FunctionalExtensionality.
 
-Program Instance [ ? EqDec (@eq_setoid A) ] => bool_function_eqdec : ? EqDec (@eq_setoid (bool -> A)) :=
+Program Instance [ EqDec (@eq_setoid A) ] => bool_function_eqdec : EqDec (@eq_setoid (bool -> A)) :=
   equiv_dec f g := 
     if f true == g true then
       if f false == g false then left
diff --git a/theories/Classes/SetoidTactics.v b/theories/Classes/SetoidTactics.v
index 953296c28..1277dcda9 100644
--- a/theories/Classes/SetoidTactics.v
+++ b/theories/Classes/SetoidTactics.v
@@ -32,5 +32,4 @@ Axiom setoideq_eq : forall [ sa : Setoid a ] (x y : a), x == y -> x = y.
 Ltac setoid_extensionality :=
   match goal with
     [ |- @eq ?A ?X ?Y ] => apply (setoideq_eq (a:=A) (x:=X) (y:=Y))
-  end.
-
+  end.
\ No newline at end of file