Implicit argument of Logic.eq become maximally inserted

  This allow in particular to write eq instead of (@eq _) in
  signatures of morphisms. I dont really see how this could
  break existing code, no change in the stdlib was mandatory.
  We'll check the contribs tomorrow...

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

9 files changed, 33 insertions, 32 deletions

diff --git a/CHANGES b/CHANGES
index a65195e15c..72ef742f48 100644
--- a/CHANGES
+++ b/CHANGES
@@ -88,6 +88,8 @@ Library
   instead of relying on lt_eq_lt_dec. The earlier version is still
   available under the name nat_compare_alt.
 - Lemmas in library Reals have been homogenized a bit.
+- The implicit argument of Logic.eq is now maximally inserted, allowing
+  to simply write "eq" instead of "@eq _" in morphism signatures. 
 
 Changes from V8.1 to V8.2
 =========================
diff --git a/theories/Classes/Morphisms.v b/theories/Classes/Morphisms.v
index 656b9d74ec..fe2f553113 100644
--- a/theories/Classes/Morphisms.v
+++ b/theories/Classes/Morphisms.v
@@ -148,7 +148,7 @@ Ltac proper_subrelation :=
 Hint Extern 5 (@Proper _ ?H _) => proper_subrelation : typeclass_instances.
 
 Instance proper_subrelation_proper :
-  Proper (subrelation ++> @eq _ ==> impl) (@Proper A).
+  Proper (subrelation ++> eq ==> impl) (@Proper A).
 Proof. reduce. subst. firstorder. Qed.
 
 (** Essential subrelation instances for [iff], [impl] and [pointwise_relation]. *)
@@ -433,7 +433,7 @@ Hint Extern 1 (subrelation _ (flip _)) => class_apply @inverse2 : typeclass_inst
 Lemma eq_subrelation `(Reflexive A R) : subrelation (@eq A) R.
 Proof. simpl_relation. Qed.
 
-(* Hint Extern 3 (subrelation (@eq _) ?R) => not_evar R ; class_apply eq_subrelation : typeclass_instances. *)
+(* Hint Extern 3 (subrelation eq ?R) => not_evar R ; class_apply eq_subrelation : typeclass_instances. *)
 
 (** Once we have normalized, we will apply this instance to simplify the problem. *)
 
@@ -443,7 +443,7 @@ Hint Extern 2 (@Proper _ (flip _) _) => class_apply @proper_inverse_proper : typ
 
 (** Bootstrap !!! *)
 
-Instance proper_proper : Proper (relation_equivalence ==> @eq _ ==> iff) (@Proper A).
+Instance proper_proper : Proper (relation_equivalence ==> eq ==> iff) (@Proper A).
 Proof.
   simpl_relation.
   reduce in H.
diff --git a/theories/FSets/FMapFacts.v b/theories/FSets/FMapFacts.v
index 88ca717e2b..10924769e9 100644
--- a/theories/FSets/FMapFacts.v
+++ b/theories/FSets/FMapFacts.v
@@ -22,9 +22,6 @@ Unset Strict Implicit.
 
 Hint Extern 1 (Equivalence _) => constructor; congruence.
 
-Notation Leibniz := (@eq _) (only parsing).
-
-
 (** * Facts about weak maps *)
 
 Module WFacts_fun (E:DecidableType)(Import M:WSfun E).
@@ -673,7 +670,7 @@ rewrite (In_iff m Hk), in_find_iff, in_find_iff, Hm; intuition.
 Qed.
 
 Add Parametric Morphism elt : (@MapsTo elt)
- with signature E.eq ==> Leibniz ==> Equal ==> iff as MapsTo_m.
+ with signature E.eq ==> eq ==> Equal ==> iff as MapsTo_m.
 Proof.
 unfold Equal; intros k k' Hk e m m' Hm.
 rewrite (MapsTo_iff m e Hk), find_mapsto_iff, find_mapsto_iff, Hm;
@@ -689,28 +686,28 @@ rewrite Hm in H0; eauto.
 Qed.
 
 Add Parametric Morphism elt : (@is_empty elt)
- with signature Equal ==> Leibniz as is_empty_m.
+ with signature Equal ==> eq as is_empty_m.
 Proof.
 intros m m' Hm.
 rewrite eq_bool_alt, <-is_empty_iff, <-is_empty_iff, Hm; intuition.
 Qed.
 
 Add Parametric Morphism elt : (@mem elt)
- with signature E.eq ==> Equal ==> Leibniz as mem_m.
+ with signature E.eq ==> Equal ==> eq as mem_m.
 Proof.
 intros k k' Hk m m' Hm.
 rewrite eq_bool_alt, <- mem_in_iff, <-mem_in_iff, Hk, Hm; intuition.
 Qed.
 
 Add Parametric Morphism elt : (@find elt)
- with signature E.eq ==> Equal ==> Leibniz as find_m.
+ with signature E.eq ==> Equal ==> eq as find_m.
 Proof.
 intros k k' Hk m m' Hm. rewrite eq_option_alt. intro e.
 rewrite <- 2 find_mapsto_iff, Hk, Hm. split; auto.
 Qed.
 
 Add Parametric Morphism elt : (@add elt)
- with signature E.eq ==> Leibniz ==> Equal ==> Equal as add_m.
+ with signature E.eq ==> eq ==> Equal ==> Equal as add_m.
 Proof.
 intros k k' Hk e m m' Hm y.
 rewrite add_o, add_o; do 2 destruct eq_dec; auto.
@@ -728,7 +725,7 @@ elim n; rewrite Hk; auto.
 Qed.
 
 Add Parametric Morphism elt elt' : (@map elt elt')
- with signature Leibniz ==> Equal ==> Equal as map_m.
+ with signature eq ==> Equal ==> Equal as map_m.
 Proof.
 intros f m m' Hm y.
 rewrite map_o, map_o, Hm; auto.
@@ -1036,7 +1033,7 @@ Module WProperties_fun (E:DecidableType)(M:WSfun E).
   (** This is more convenient than a [compat_op eqke ...].
       In fact, every [compat_op], [compat_bool], etc, should
       become a [Proper] someday. *)
-  Hypothesis Comp : Proper (E.eq==>Leibniz==>eqA==>eqA) f.
+  Hypothesis Comp : Proper (E.eq==>eq==>eqA==>eqA) f.
 
   Lemma fold_init :
    forall m i i', eqA i i' -> eqA (fold f m i) (fold f m i').
@@ -1189,7 +1186,7 @@ Module WProperties_fun (E:DecidableType)(M:WSfun E).
     Equal m m' -> cardinal m = cardinal m'.
   Proof.
   intros; do 2 rewrite cardinal_fold.
-  apply fold_Equal with (eqA:=Leibniz); compute; auto.
+  apply fold_Equal with (eqA:=eq); compute; auto.
   Qed.
 
   Lemma cardinal_1 : forall m : t elt, Empty m -> cardinal m = 0.
@@ -1202,7 +1199,7 @@ Module WProperties_fun (E:DecidableType)(M:WSfun E).
   Proof.
   intros; do 2 rewrite cardinal_fold.
   change S with ((fun _ _ => S) x e).
-  apply fold_Add with (eqA:=Leibniz); compute; auto.
+  apply fold_Add with (eqA:=eq); compute; auto.
   Qed.
 
   Lemma cardinal_inv_1 : forall m : t elt,
@@ -1273,7 +1270,7 @@ Module WProperties_fun (E:DecidableType)(M:WSfun E).
 
   Section Specs.
   Variable f : key -> elt -> bool.
-  Hypothesis Hf : Proper (E.eq==>Leibniz==>Leibniz) f.
+  Hypothesis Hf : Proper (E.eq==>eq==>eq) f.
 
   Lemma filter_iff : forall m k e,
    MapsTo k e (filter f m) <-> MapsTo k e m /\ f k e = true.
@@ -1366,7 +1363,7 @@ Module WProperties_fun (E:DecidableType)(M:WSfun E).
 
   Section Partition.
   Variable f : key -> elt -> bool.
-  Hypothesis Hf : Proper (E.eq==>Leibniz==>Leibniz) f.
+  Hypothesis Hf : Proper (E.eq==>eq==>eq) f.
 
   Lemma partition_iff_1 : forall m m1 k e,
    m1 = fst (partition f m) ->
@@ -1495,7 +1492,7 @@ Module WProperties_fun (E:DecidableType)(M:WSfun E).
 
   Lemma Partition_fold :
    forall (A:Type)(eqA:A->A->Prop)(st:Equivalence eqA)(f:key->elt->A->A),
-   Proper (E.eq==>Leibniz==>eqA==>eqA) f ->
+   Proper (E.eq==>eq==>eqA==>eqA) f ->
    transpose_neqkey eqA f ->
    forall m m1 m2 i,
    Partition m m1 m2 ->
@@ -1549,7 +1546,7 @@ Module WProperties_fun (E:DecidableType)(M:WSfun E).
   setoid_replace (fold f m 0) with (fold f m1 (fold f m2 0)).
   rewrite <- cardinal_fold.
   intros. apply fold_rel with (R:=fun u v => u = v + cardinal m2); simpl; auto.
-  apply Partition_fold with (eqA:=@Logic.eq _); try red; auto.
+  apply Partition_fold with (eqA:=eq); try red; auto.
   compute; auto.
   Qed.
 
@@ -1558,7 +1555,7 @@ Module WProperties_fun (E:DecidableType)(M:WSfun E).
    Equal m1 (fst (partition f m)) /\ Equal m2 (snd (partition f m)).
   Proof.
   intros m m1 m2 Hm f.
-  assert (Hf : Proper (E.eq==>Leibniz==>Leibniz) f).
+  assert (Hf : Proper (E.eq==>eq==>eq) f).
    intros k k' Hk e e' _; unfold f; rewrite Hk; auto.
   set (m1':= fst (partition f m)).
   set (m2':= snd (partition f m)).
@@ -1674,7 +1671,7 @@ Module WProperties_fun (E:DecidableType)(M:WSfun E).
  End Elt.
 
  Add Parametric Morphism elt : (@cardinal elt)
-   with signature Equal ==> Leibniz as cardinal_m.
+   with signature Equal ==> eq as cardinal_m.
  Proof. intros; apply Equal_cardinal; auto. Qed.
 
  Add Parametric Morphism elt : (@Disjoint elt)
@@ -2151,7 +2148,7 @@ Module OrdProperties (M:S).
 
   Lemma fold_Equal : forall m1 m2 (A:Type)(eqA:A->A->Prop)(st:Equivalence  eqA)
    (f:key->elt->A->A)(i:A),
-   Proper (E.eq==>Leibniz==>eqA==>eqA) f ->
+   Proper (E.eq==>eq==>eqA==>eqA) f ->
    Equal m1 m2 ->
    eqA (fold f m1 i) (fold f m2 i).
   Proof.
@@ -2164,7 +2161,7 @@ Module OrdProperties (M:S).
   Qed.
 
   Lemma fold_Add_Above : forall m1 m2 x e (A:Type)(eqA:A->A->Prop)(st:Equivalence eqA)
-   (f:key->elt->A->A)(i:A) (P:Proper (E.eq==>Leibniz==>eqA==>eqA) f),
+   (f:key->elt->A->A)(i:A) (P:Proper (E.eq==>eq==>eqA==>eqA) f),
    Above x m1 -> Add x e m1 m2 ->
    eqA (fold f m2 i) (f x e (fold f m1 i)).
   Proof.
@@ -2180,7 +2177,7 @@ Module OrdProperties (M:S).
   Qed.
 
   Lemma fold_Add_Below : forall m1 m2 x e (A:Type)(eqA:A->A->Prop)(st:Equivalence eqA)
-   (f:key->elt->A->A)(i:A) (P:Proper (E.eq==>Leibniz==>eqA==>eqA) f),
+   (f:key->elt->A->A)(i:A) (P:Proper (E.eq==>eq==>eqA==>eqA) f),
    Below x m1 -> Add x e m1 m2 ->
    eqA (fold f m2 i) (fold f m1 (f x e i)).
   Proof.
diff --git a/theories/FSets/FSetEqProperties.v b/theories/FSets/FSetEqProperties.v
index d843bbcd60..c95aa80254 100644
--- a/theories/FSets/FSetEqProperties.v
+++ b/theories/FSets/FSetEqProperties.v
@@ -837,8 +837,8 @@ Section Sum.
 (** Adding a valuation function on all elements of a set. *)
 
 Definition sum (f:elt -> nat)(s:t) := fold (fun x => plus (f x)) s 0.
-Notation compat_opL := (compat_op E.eq (@Logic.eq _)).
-Notation transposeL := (transpose (@Logic.eq _)).
+Notation compat_opL := (compat_op E.eq Logic.eq).
+Notation transposeL := (transpose Logic.eq).
 
 Lemma sum_plus :
   forall f g, compat_nat E.eq f -> compat_nat E.eq g ->
diff --git a/theories/Init/Logic.v b/theories/Init/Logic.v
index ede73ebf14..e1bb443a63 100644
--- a/theories/Init/Logic.v
+++ b/theories/Init/Logic.v
@@ -251,6 +251,8 @@ Notation "x = y" := (x = y :>_) : type_scope.
 Notation "x <> y  :> T" := (~ x = y :>T) : type_scope.
 Notation "x <> y" := (x <> y :>_) : type_scope.
 
+Implicit Arguments eq [ [A] ].
+
 Implicit Arguments eq_ind [A].
 Implicit Arguments eq_rec [A].
 Implicit Arguments eq_rect [A].
diff --git a/theories/Lists/StreamMemo.v b/theories/Lists/StreamMemo.v
index e8b9358413..e10ad325f8 100644
--- a/theories/Lists/StreamMemo.v
+++ b/theories/Lists/StreamMemo.v
@@ -97,7 +97,7 @@ match v with
 | memo_mval m x =>
     match is_eq n m with
     | left H =>
-       match H in (@eq _ _ y) return (A y -> A n) with
+       match H in (eq _ y) return (A y -> A n) with
         | refl_equal => fun v1 : A n => v1
        end
     | right _ => fun _ : A m => f n
diff --git a/theories/Numbers/Natural/Abstract/NBase.v b/theories/Numbers/Natural/Abstract/NBase.v
index deee349ca2..c7632d1859 100644
--- a/theories/Numbers/Natural/Abstract/NBase.v
+++ b/theories/Numbers/Natural/Abstract/NBase.v
@@ -81,7 +81,7 @@ function (by recursion) that maps 0 to false and the successor to true *)
 Definition if_zero (A : Set) (a b : A) (n : N) : A :=
   recursion a (fun _ _ => b) n.
 
-Add Parametric Morphism (A : Set) : (if_zero A) with signature (@eq _ ==> @eq _ ==> Neq ==> @eq _) as if_zero_wd.
+Add Parametric Morphism (A : Set) : (if_zero A) with signature (eq ==> eq ==> Neq ==> eq) as if_zero_wd.
 Proof.
 intros; unfold if_zero. apply recursion_wd with (Aeq := (@eq A)).
 reflexivity. unfold fun2_eq; now intros. assumption.
diff --git a/theories/QArith/QArith_base.v b/theories/QArith/QArith_base.v
index dff556b98f..c87c9df9ef 100644
--- a/theories/QArith/QArith_base.v
+++ b/theories/QArith/QArith_base.v
@@ -835,7 +835,7 @@ Qed.
 Definition Qpower_positive (q:Q)(p:positive) : Q :=
  pow_pos Qmult q p.
 
-Add Morphism Qpower_positive with signature Qeq ==> @eq _ ==> Qeq as Qpower_positive_comp.
+Add Morphism Qpower_positive with signature Qeq ==> eq ==> Qeq as Qpower_positive_comp.
 Proof.
 intros x1 x2 Hx y.
 unfold Qpower_positive.
@@ -854,7 +854,7 @@ Definition Qpower (q:Q) (z:Z) :=
 
 Notation " q ^ z " := (Qpower q z) : Q_scope.
 
-Add Morphism Qpower with signature Qeq ==> @eq _ ==> Qeq as Qpower_comp.
+Add Morphism Qpower with signature Qeq ==> eq ==> Qeq as Qpower_comp.
 Proof.
 intros x1 x2 Hx [|y|y]; try reflexivity;
 simpl; rewrite Hx; reflexivity.
diff --git a/theories/QArith/Qround.v b/theories/QArith/Qround.v
index 3f191c7523..8162a702fa 100644
--- a/theories/QArith/Qround.v
+++ b/theories/QArith/Qround.v
@@ -122,7 +122,7 @@ Qed.
 
 Hint Resolve Qceiling_resp_le : qarith.
 
-Add Morphism Qfloor with signature Qeq ==> @eq _ as Qfloor_comp.
+Add Morphism Qfloor with signature Qeq ==> eq as Qfloor_comp.
 Proof.
 intros x y H.
 apply Zle_antisym.
@@ -130,7 +130,7 @@ apply Zle_antisym.
 symmetry in H; auto with *.
 Qed.
 
-Add Morphism Qceiling with signature Qeq ==> @eq _ as Qceiling_comp.
+Add Morphism Qceiling with signature Qeq ==> eq as Qceiling_comp.
 Proof.
 intros x y H.
 apply Zle_antisym.