Fix bugs that were reopened due to the change of setoid

implementation. Mostly syntax changes when declaring parametric
relations, but also some declarations were relying on "default"
relations on some carrier. Added a new DefaultRelation type class that
allows to do that, falling back to the last declared Equivalence
relation by default. This will be bound to Add Relation in the next
commit. 

Also, move the "left" and "right" notations in Program.Utils to "in_left" and
"in_right" to avoid clashes with existing scripts.

Minor change to record to allow choosing the name of the argument for
the record in projections to avoid possible incompatibilities.


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

20 files changed, 188 insertions, 135 deletions

diff --git a/CHANGES b/CHANGES
index 3bba84fc75..d1e60f33ba 100644
--- a/CHANGES
+++ b/CHANGES
@@ -159,6 +159,9 @@ Program
   they can be automatically solved by the default tactic.
 - New command "Preterm [ of id ]" to see the actual term fed to Coq for
   debugging purposes.
+- Changed the notations "left" and "right" to "in_left" and "in_right" to hide the 
+  proofs in standard disjunctions, to avoid breaking existing scripts when importing
+  Program. Also, put them in program_scope.
   
 Miscellaneous
 
diff --git a/Makefile.common b/Makefile.common
index d4dc8256f0..5e35108dbc 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -748,8 +748,8 @@ SETOIDSVO:= theories/Setoids/Setoid.vo # theories/Setoids/Setoid_tac.vo theories
 UNICODEVO:= theories/Unicode/Utf8.vo
 
 CLASSESVO:= theories/Classes/Init.vo theories/Classes/Relations.vo theories/Classes/Morphisms.vo \
-	theories/Classes/Functions.vo theories/Classes/Equivalence.vo \
-	theories/Classes/SetoidClass.vo theories/Classes/SetoidTactics.vo theories/Classes/SetoidDec.vo
+	theories/Classes/Functions.vo theories/Classes/Equivalence.vo theories/Classes/SetoidTactics.vo \
+	theories/Classes/SetoidClass.vo theories/Classes/SetoidAxioms.vo theories/Classes/SetoidDec.vo
 
 THEORIESVO:=\
   $(INITVO) $(LOGICVO) $(ARITHVO) $(BOOLVO) $(NARITHVO) $(ZARITHVO) \
diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4
index bb73d40948..aa509ba771 100644
--- a/tactics/class_tactics.ml4
+++ b/tactics/class_tactics.ml4
@@ -368,6 +368,7 @@ let respectful_dep = lazy (gen_constant ["Classes"; "Morphisms"] "respectful_dep
 let respectful = lazy (gen_constant ["Classes"; "Morphisms"] "respectful")
 
 let equivalence = lazy (gen_constant ["Classes"; "Relations"] "Equivalence")
+let default_relation = lazy (gen_constant ["Classes"; "Relations"] "DefaultRelation")
 
 let iff_equiv = lazy (gen_constant ["Classes"; "Relations"] "iff_equivalence")
 let eq_equiv = lazy (gen_constant ["Classes"; "SetoidClass"] "eq_equivalence")
@@ -858,8 +859,14 @@ let require_library dirpath =
   let qualid = (dummy_loc, Libnames.qualid_of_dirpath (Libnames.dirpath_of_string dirpath)) in
     Library.require_library [qualid] (Some false)
 
+let check_required_library d =
+  let d' = List.map id_of_string d in
+  let dir = make_dirpath (List.rev d') in
+  if not (Library.library_is_opened dir) then
+    error ("Library "^(list_last d)^" has to be required first")
+
 let init_setoid () =
-  require_library "Coq.Setoids.Setoid"
+  check_required_library ["Coq";"Setoids";"Setoid"]
 
 let declare_instance_refl a aeq n lemma = 
   let instance = declare_instance a aeq (add_suffix n "_refl") "Reflexive" 
@@ -1029,9 +1036,9 @@ let build_morphism_signature m =
   in
   let sig_, evars = build_signature isevars env t cstrs snd in
   let _ = List.iter 
-    (fun (ty, relty) -> 
-      let equiv = mkApp (Lazy.force equivalence, [| ty; relty |]) in
-	ignore(Evarutil.e_new_evar isevars env equiv))
+    (fun (ty, rel) -> 
+      let default = mkApp (Lazy.force default_relation, [| ty; rel |]) in
+	ignore(Evarutil.e_new_evar isevars env default))
     evars
   in
   let morph = 
diff --git a/test-suite/bugs/closed/shouldsucceed/1634.v b/test-suite/bugs/closed/shouldsucceed/1634.v
index 9e50f6f252..205e827982 100644
--- a/test-suite/bugs/closed/shouldsucceed/1634.v
+++ b/test-suite/bugs/closed/shouldsucceed/1634.v
@@ -3,22 +3,22 @@ Require Export Setoid.
 
 Variable A : Type.
 Variable S : A -> Type.
-Variable Seq : forall (a:A), relation (S a).
+Variable Seq : forall {a:A}, relation (S a).
 
-Hypothesis Seq_refl : forall (a:A) (x : S a), Seq a x x.
-Hypothesis Seq_sym : forall (a:A) (x y : S a), Seq a x y -> Seq a y x.
-Hypothesis Seq_trans : forall (a:A) (x y z : S a), Seq a x y -> Seq a y z ->
-Seq
-a x z.
+Hypothesis Seq_refl : forall {a:A} (x : S a), Seq x x.
+Hypothesis Seq_sym : forall {a:A} (x y : S a), Seq x y -> Seq y x.
+Hypothesis Seq_trans : forall {a:A} (x y z : S a), Seq x y -> Seq y z ->
+Seq x z.
 
-Add Relation S Seq
+Add Relation (S a) Seq
  reflexivity proved by Seq_refl
  symmetry proved by Seq_sym
  transitivity proved by Seq_trans
  as S_Setoid.
 
-Goal forall (a : A) (x y : S a), Seq a x y -> Seq a x y.
+Goal forall (a : A) (x y : S a), Seq x y -> Seq x y.
   intros a x y H.
-  setoid_replace x with y using relation Seq.
-  apply Seq_refl. trivial.
+  setoid_replace x with y. 
+  reflexivity.
+  trivial.
 Qed.
diff --git a/test-suite/bugs/closed/shouldsucceed/846.v b/test-suite/bugs/closed/shouldsucceed/846.v
index a963b225fe..95bbab92a3 100644
--- a/test-suite/bugs/closed/shouldsucceed/846.v
+++ b/test-suite/bugs/closed/shouldsucceed/846.v
@@ -138,15 +138,15 @@ Proof.
   right; assumption.
   intros l _ r.
   apply (step (A:=L' A l)).
-  exact (inl _ (inl _ r)).
+  exact (inl (inl r)).
   intros l _ r1 _ r2.
   apply (step (A:=L' A l)).
   (* unfold L' in * |- *.
   Check 0. *)
-  exact (inl _ (inr _ (pair r1 r2))).
+  exact (inl (inr (pair r1 r2))).
   intros l _ r.
   apply  (step (A:=L' A l)).
-  exact (inr _ r).
+  exact (inr r).
 Defined.
 
 Definition L'inG: forall A: Set, L' A (true::nil) -> G A.
diff --git a/test-suite/output/ZSyntax.out b/test-suite/output/ZSyntax.out
index cbfb9f207b..a24ad124eb 100644
--- a/test-suite/output/ZSyntax.out
+++ b/test-suite/output/ZSyntax.out
@@ -2,19 +2,19 @@
      : Z
 fun f : nat -> Z => (f 0%nat + 0)%Z
      : (nat -> Z) -> Z
-fun x : positive => Zpos (xO x)
+fun x : positive => Zpos x~0)
      : positive -> Z
 fun x : positive => (Zpos x + 1)%Z
      : positive -> Z
 fun x : positive => Zpos x
      : positive -> Z
-fun x : positive => Zneg (xO x)
+fun x : positive => Zneg x~0
      : positive -> Z
-fun x : positive => (Zpos (xO x) + 0)%Z
+fun x : positive => (Zpos x~0 + 0)%Z
      : positive -> Z
-fun x : positive => (- Zpos (xO x))%Z
+fun x : positive => (- Zpos x~0)%Z
      : positive -> Z
-fun x : positive => (- Zpos (xO x) + 0)%Z
+fun x : positive => (- Zpos x~0 + 0)%Z
      : positive -> Z
 (Z_of_nat 0 + 1)%Z
      : Z
diff --git a/test-suite/success/extraction.v b/test-suite/success/extraction.v
index 0b3060d519..6a5bf58b64 100644
--- a/test-suite/success/extraction.v
+++ b/test-suite/success/extraction.v
@@ -84,7 +84,7 @@ Extraction test12.
 (* type test12 = (__ -> __ -> __) -> __ *)
 
 
-Definition test13 := match left True I with
+Definition test13 := match @left True True I with
                      | left x => 1
                      | right x => 0
                      end.
@@ -322,7 +322,7 @@ Extraction test24.
 Require Import Gt.
 Definition loop (Ax:Acc gt 0) :=
   (fix F (a:nat) (b:Acc gt a) {struct b} : nat :=
-     F (S a) (Acc_inv b (S a) (gt_Sn_n a))) 0 Ax.
+     F (S a) (Acc_inv b (gt_Sn_n a))) 0 Ax.
 Extraction loop.
 (* let loop _ =
   let rec f a =
diff --git a/test-suite/success/setoid_test.v b/test-suite/success/setoid_test.v
index e99b3c19bb..2be1500f4e 100644
--- a/test-suite/success/setoid_test.v
+++ b/test-suite/success/setoid_test.v
@@ -110,9 +110,9 @@ Definition id: Set -> Set := fun A => A.
 Definition rel : forall A : Set, relation (id A) := @eq.
 Definition f: forall A : Set, A -> A := fun A x => x.
 
-Add Relation id rel as eq_rel.
+Instance DefaultRelation (id A) (rel A).
 
-Add Morphism f with signature rel ++> rel as f_morph.
+Add Morphism (@f A) : f_morph.
 Proof.
 unfold rel, f. trivial.
 Qed.
diff --git a/test-suite/success/setoid_test2.v b/test-suite/success/setoid_test2.v
index bac1cf1493..8e5729dce0 100644
--- a/test-suite/success/setoid_test2.v
+++ b/test-suite/success/setoid_test2.v
@@ -120,6 +120,8 @@ Axiom eqS1: S1 -> S1 -> Prop.
 Axiom SetoidS1 : Setoid_Theory S1 eqS1.
 Add Setoid S1 eqS1 SetoidS1 as S1setoid.
 
+Instance DefaultRelation S1 eqS1.
+
 Axiom eqS1': S1 -> S1 -> Prop.
 Axiom SetoidS1' : Setoid_Theory S1 eqS1'.
 Axiom SetoidS1'_bis : Setoid_Theory S1 eqS1'.
@@ -218,6 +220,8 @@ Axiom eqS1_test8: S1_test8 -> S1_test8 -> Prop.
 Axiom SetoidS1_test8 : Setoid_Theory S1_test8 eqS1_test8.
 Add Setoid S1_test8 eqS1_test8 SetoidS1_test8 as S1_test8setoid.
 
+Instance DefaultRelation S1_test8 eqS1_test8.
+
 Axiom f_test8 : S2 -> S1_test8.
 Add Morphism f_test8 : f_compat_test8. Admitted.
 
diff --git a/test-suite/success/setoid_test_function_space.v b/test-suite/success/setoid_test_function_space.v
index 1602991df2..2e9bd60ea7 100644
--- a/test-suite/success/setoid_test_function_space.v
+++ b/test-suite/success/setoid_test_function_space.v
@@ -26,14 +26,14 @@ Hint Unfold feq. Hint Resolve feq_refl feq_sym feq_trans.
 Variable K:(nat -> nat)->Prop.
 Variable K_ext:forall a b, (K a)->(a =f b)->(K b).
 
-Add Relation (fun A B:Type => A -> B) feq
- reflexivity proved by feq_refl
- symmetry proved by feq_sym
- transitivity proved by feq_trans as funsetoid.
+Add Relation (A -> B) (@feq A B)
+ reflexivity proved by (@feq_refl A B)
+ symmetry proved by (@feq_sym A B)
+ transitivity proved by (@feq_trans A B) as funsetoid.
                                                                              
-Add Morphism K with signature feq ==> iff as K_ext1.
+Add Morphism K with signature (@feq nat nat) ==> iff as K_ext1.
 intuition. apply (K_ext H0 H).
-intuition. assert (x2 =f x1);auto.  apply (K_ext H0 H1).
+intuition. assert (y =f x);auto.  apply (K_ext H0 H1).
 Qed.
 
 Lemma three:forall n, forall a, (K a)->(a =f (fun m => (a (n+m))))-> (K (fun m
diff --git a/theories/Classes/Equivalence.v b/theories/Classes/Equivalence.v
index da302ea9d0..a19f8da82d 100644
--- a/theories/Classes/Equivalence.v
+++ b/theories/Classes/Equivalence.v
@@ -22,6 +22,7 @@ Require Import Coq.Program.Program.
 Require Import Coq.Classes.Init.
 Require Export Coq.Classes.Relations.
 Require Export Coq.Classes.Morphisms.
+Require Export Coq.Classes.SetoidTactics.
 
 Set Implicit Arguments.
 Unset Strict Implicit.
@@ -47,7 +48,7 @@ Proof. eauto with typeclass_instances. Qed.
 Notation " x === y " := (equiv x y) (at level 70, no associativity) : equiv_scope.
 
 Notation " x =/= y " := (complement equiv x y) (at level 70, no associativity) : equiv_scope.
-
+  
 Open Local Scope equiv_scope.
 
 (** Use the [clsubstitute] command which substitutes an equality in every hypothesis. *)
@@ -67,66 +68,6 @@ Ltac clsubst_nofail :=
 
 Tactic Notation "clsubst" "*" := clsubst_nofail.
 
-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.
-
-
-Ltac red_subst_eq_morphism concl :=
-  match concl with
-    | @Logic.eq ?A ==> ?R' => red ; intros ; subst ; red_subst_eq_morphism R'
-    | ?R ==> ?R' => red ; intros ; red_subst_eq_morphism R'
-    | _ => idtac
-  end.
-
-Ltac destruct_morphism :=
-  match goal with
-    | [ |- @Morphism ?A ?R ?m ] => constructor
-  end.
-
-Ltac reverse_arrows x :=
-  match x with
-    | @Logic.eq ?A ==> ?R' => revert_last ; reverse_arrows R'
-    | ?R ==> ?R' => do 3 revert_last ; reverse_arrows R'
-    | _ => idtac
-  end.
-
-Ltac add_morphism_tactic := (try destruct_morphism) ;
-  match goal with
-    | [ |- (?x ==> ?y) _ _ ] => red_subst_eq_morphism (x ==> y) ; reverse_arrows (x ==> y)
-  end.
-  
 Lemma nequiv_equiv_trans : forall [ ! Equivalence A ] (x y z : A), x =/= y -> y === z -> x =/= z.
 Proof with auto.
   intros; intro.
@@ -196,21 +137,17 @@ Program Instance iff_impl_id_morphism :
 Class PartialEquivalence (carrier : Type) (pequiv : relation carrier) :=
   pequiv_prf :> PER carrier pequiv.
 
+Definition pequiv [ PartialEquivalence A R ] : relation A := R.
+
 (** Overloaded notation for partial equiv equivalence. *)
 
-(* Infix "=~=" := pequiv (at level 70, no associativity) : type_scope. *)
+Notation " x =~= y " := (pequiv x y) (at level 70, no associativity) : type_scope.
 
 (** 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.
-
+  equivalence_default : DefaultRelation A R | 4.
diff --git a/theories/Classes/Relations.v b/theories/Classes/Relations.v
index b14647d065..530f21264b 100644
--- a/theories/Classes/Relations.v
+++ b/theories/Classes/Relations.v
@@ -24,6 +24,17 @@ Unset Strict Implicit.
 
 Notation "'relation' A " := (A -> A -> Prop) (at level 0).
 
+(** Default relation on a given support. *)
+
+Class DefaultRelation A (R : relation A).
+
+(** To search for the default relation, just call [default_relation]. *)
+
+Definition default_relation [ DefaultRelation A R ] : relation A := R.
+
+(** A notation for applying the default relation to [x] and [y]. *)
+Notation " x ===def y " := (default_relation x y) (at level 70, no associativity).
+
 Definition inverse A (R : relation A) : relation A := fun x y => R y x.
 
 Lemma inverse_inverse : forall A (R : relation A), inverse (inverse R) = R.
diff --git a/theories/Classes/SetoidAxioms.v b/theories/Classes/SetoidAxioms.v
new file mode 100644
index 0000000000..6b7881c9f2
--- /dev/null
+++ b/theories/Classes/SetoidAxioms.v
@@ -0,0 +1,35 @@
+(* -*- coq-prog-args: ("-emacs-U" "-nois") -*- *)
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(* Extensionality axioms that can be used when reasoning with setoids.
+ *
+ * Author: Matthieu Sozeau
+ * Institution: LRI, CNRS UMR 8623 - UniversitÃcopyright Paris Sud
+ *              91405 Orsay, France *)
+
+(* $Id: FSetAVL_prog.v 616 2007-08-08 12:28:10Z msozeau $ *)
+
+Require Import Coq.Program.Program.
+
+Set Implicit Arguments.
+Unset Strict Implicit.
+
+Require Export Coq.Classes.SetoidClass.
+
+(* Application of the extensionality axiom to turn a goal on leibinz equality to 
+   a setoid equivalence. *)
+
+Axiom setoideq_eq : forall [ sa : Setoid a ] (x y : a), x == y -> x = y.
+
+(** Application of the extensionality principle for setoids. *)
+
+Ltac setoid_extensionality :=
+  match goal with
+    [ |- @eq ?A ?X ?Y ] => apply (setoideq_eq (a:=A) (x:=X) (y:=Y))
+  end.
\ No newline at end of file
diff --git a/theories/Classes/SetoidDec.v b/theories/Classes/SetoidDec.v
index 8a435b4493..86a2bef80f 100644
--- a/theories/Classes/SetoidDec.v
+++ b/theories/Classes/SetoidDec.v
@@ -50,6 +50,8 @@ Definition swap_sumbool {A B} (x : { A } + { B }) : { B } + { A } :=
 
 Require Import Coq.Program.Program.
 
+Open Local Scope program_scope.
+
 (** Invert the branches. *)
 
 Program Definition nequiv_dec [ ! EqDec A ] (x y : A) : { x =/= y } + { x == y } := swap_sumbool (x == y).
@@ -87,7 +89,7 @@ Program Instance bool_eqdec : EqDec (@eq_setoid bool) :=
   equiv_dec := bool_dec.
 
 Program Instance unit_eqdec : EqDec (@eq_setoid unit) :=
-  equiv_dec x y := left.
+  equiv_dec x y := in_left.
 
   Next Obligation.
   Proof.
@@ -101,9 +103,9 @@ Program Instance [ EqDec (@eq_setoid A), EqDec (@eq_setoid B) ] =>
     dest x as (x1, x2) in 
     dest y as (y1, y2) in 
     if x1 == y1 then 
-      if x2 == y2 then left
-      else right
-    else right.
+      if x2 == y2 then in_left
+      else in_right
+    else in_right.
 
   Solve Obligations using unfold complement ; program_simpl.
 
@@ -114,9 +116,9 @@ Require Import Coq.Program.FunctionalExtensionality.
 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
-      else right
-    else right.
+      if f false == g false then in_left
+      else in_right
+    else in_right.
 
   Solve Obligations using try red ; unfold equiv, complement ; program_simpl.
 
diff --git a/theories/Classes/SetoidTactics.v b/theories/Classes/SetoidTactics.v
index 1277dcda9a..c71db69952 100644
--- a/theories/Classes/SetoidTactics.v
+++ b/theories/Classes/SetoidTactics.v
@@ -15,21 +15,80 @@
 
 (* $Id: FSetAVL_prog.v 616 2007-08-08 12:28:10Z msozeau $ *)
 
-Require Import Coq.Program.Program.
+Require Export Coq.Classes.Relations.
+Require Export Coq.Classes.Morphisms.
 
 Set Implicit Arguments.
 Unset Strict Implicit.
 
-Require Export Coq.Classes.SetoidClass.
+(** The setoid_replace tactics in Ltac, defined in terms of default relations [===def] and
+   the setoid_rewrite tactic. *)
 
-(* Application of the extensionality axiom to turn a goal on leibinz equality to 
-   a setoid equivalence. *)
+Ltac setoidreplace H t :=
+  let Heq := fresh "Heq" in
+    cut(H) ; unfold default_relation ; [ intro Heq ; setoid_rewrite Heq ; clear Heq | t ].
 
-Axiom setoideq_eq : forall [ sa : Setoid a ] (x y : a), x == y -> x = y.
+Ltac setoidreplacein H H' t :=
+  let Heq := fresh "Heq" in
+    cut(H) ; unfold default_relation ; [ intro Heq ; setoid_rewrite Heq in H' ; clear Heq | t ].
 
-(** Application of the extensionality principle for setoids. *)
+Tactic Notation "setoid_replace" constr(x) "with" constr(y) :=
+  setoidreplace (x ===def y) idtac.
 
-Ltac setoid_extensionality :=
+Tactic Notation "setoid_replace" constr(x) "with" constr(y) "in" hyp(id) :=
+  setoidreplacein (x ===def y) id idtac.
+
+Tactic Notation "setoid_replace" constr(x) "with" constr(y) "by" tactic(t) :=
+  setoidreplace (x ===def y) ltac:t.
+
+Tactic Notation "setoid_replace" constr(x) "with" constr(y) "in" hyp(id) "by" tactic(t) :=
+  setoidreplacein (x ===def 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.
+
+(** The [add_morphism_tactic] tactic is run at each [Add Morphism] command before giving the hand back
+   to the user to discharge the proof. It essentially amounts to unfold the right amount of [respectful] calls
+   and substitute leibniz equalities. One can redefine it using [Ltac add_morphism_tactic ::= t]. *)
+
+Require Import Coq.Program.Tactics.
+
+Ltac red_subst_eq_morphism concl :=
+  match concl with
+    | @Logic.eq ?A ==> ?R' => red ; intros ; subst ; red_subst_eq_morphism R'
+    | ?R ==> ?R' => red ; intros ; red_subst_eq_morphism R'
+    | _ => idtac
+  end.
+
+Ltac destruct_morphism :=
   match goal with
-    [ |- @eq ?A ?X ?Y ] => apply (setoideq_eq (a:=A) (x:=X) (y:=Y))
-  end.
\ No newline at end of file
+    | [ |- @Morphism ?A ?R ?m ] => constructor
+  end.
+
+Ltac reverse_arrows x :=
+  match x with
+    | @Logic.eq ?A ==> ?R' => revert_last ; reverse_arrows R'
+    | ?R ==> ?R' => do 3 revert_last ; reverse_arrows R'
+    | _ => idtac
+  end.
+
+Ltac default_add_morphism_tactic :=
+  (try destruct_morphism) ;
+  match goal with
+    | [ |- (?x ==> ?y) _ _ ] => red_subst_eq_morphism (x ==> y) ; reverse_arrows (x ==> y)
+  end.
+
+Ltac add_morphism_tactic := default_add_morphism_tactic.
+
diff --git a/theories/Program/Utils.v b/theories/Program/Utils.v
index c514d3234d..184e3c3678 100644
--- a/theories/Program/Utils.v
+++ b/theories/Program/Utils.v
@@ -61,16 +61,10 @@ Notation "'dec'" := (sumbool_of_bool) (at level 0).
 
 (** The notations [in_right] and [in_left] construct objects of a dependent disjunction. *)
 
-
-(** These type arguments should be infered from the context. *)
-
-Implicit Arguments left [[A]].
-Implicit Arguments right [[B]].
-
 (** Hide proofs and generates obligations when put in a term. *)
 
-Notation left := (left _ _).
-Notation right := (right _ _).
+Notation "'in_left'" := (@left _ _ _) : program_scope.
+Notation "'in_right'" := (@right _ _ _) : program_scope.
 
 (** Extraction directives *)
 
diff --git a/theories/ZArith/Zdiv.v b/theories/ZArith/Zdiv.v
index ff8033eeb4..6bcbbf6b70 100644
--- a/theories/ZArith/Zdiv.v
+++ b/theories/ZArith/Zdiv.v
@@ -21,6 +21,7 @@ Require Import Zbool.
 Require Import Omega.
 Require Import ZArithRing.
 Require Import Zcomplements.
+Require Export Setoid.
 Open Local Scope Z_scope.
 
 (** * Definitions of Euclidian operations *)
diff --git a/toplevel/classes.ml b/toplevel/classes.ml
index 32803742a0..4af59ff621 100644
--- a/toplevel/classes.ml
+++ b/toplevel/classes.ml
@@ -185,7 +185,8 @@ let declare_structure env id idbuild params arity fields =
       mind_entry_inds = [mie_ind] } in
   let kn = Command.declare_mutual_with_eliminations true mie in
   let rsp = (kn,0) in (* This is ind path of idstruc *)
-  let kinds,sp_projs = Record.declare_projections rsp (List.map (fun _ -> false) fields) fields in
+  let id = Nameops.next_ident_away id (ids_of_context (Global.env())) in
+  let kinds,sp_projs = Record.declare_projections rsp ~name:id (List.map (fun _ -> false) fields) fields in
   let _build = ConstructRef (rsp,1) in
     Recordops.declare_structure(rsp,idbuild,List.rev kinds,List.rev sp_projs);
     rsp
diff --git a/toplevel/record.ml b/toplevel/record.ml
index b94dffe1a0..b045573045 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -131,15 +131,14 @@ let instantiate_possibly_recursive_type indsp paramdecls fields =
   substl_rel_context (subst@[mkInd indsp]) fields
 
 (* We build projections *)
-let declare_projections indsp coers fields =
+let declare_projections indsp ?name coers fields =
   let env = Global.env() in
   let (mib,mip) = Global.lookup_inductive indsp in
   let paramdecls = mib.mind_params_ctxt in
   let r = mkInd indsp in
   let rp = applist (r, extended_rel_list 0 paramdecls) in
   let paramargs = extended_rel_list 1 paramdecls in (*def in [[params;x:rp]]*)
-  let x = Name (next_ident_away mip.mind_typename (ids_of_context (Global.env()))) in
-    (* Termops.named_hd (Global.env()) r Anonymous  *)
+  let x = match name with Some n -> Name n | None -> Termops.named_hd (Global.env()) r Anonymous in
   let fields = instantiate_possibly_recursive_type indsp paramdecls fields in
   let lifted_fields = lift_rel_context 1 fields in
   let (_,kinds,sp_projs,_) =
diff --git a/toplevel/record.mli b/toplevel/record.mli
index e322dcfd0b..5ba8b04e1a 100644
--- a/toplevel/record.mli
+++ b/toplevel/record.mli
@@ -16,12 +16,12 @@ open Vernacexpr
 open Topconstr
 (*i*)
 
-(* [declare_projections ref coers params fields] declare projections of
-   record [ref] (if allowed), and put them as coercions accordingly to
-   [coers]; it returns the absolute names of projections *)
+(* [declare_projections ref name coers params fields] declare projections of
+   record [ref] (if allowed) using the given [name] as argument, and put them
+   as coercions accordingly to [coers]; it returns the absolute names of projections *)
 
 val declare_projections :
-  inductive -> bool list -> rel_context -> bool list * constant option list
+  inductive -> ?name:identifier -> bool list -> rel_context -> bool list * constant option list
 
 val definition_structure :
   lident with_coercion * local_binder list *