ZArith + other : favor the use of modern names instead of compat notations

 - For instance, refl_equal --> eq_refl
 - Npos, Zpos, Zneg now admit more uniform qualified aliases
   N.pos, Z.pos, Z.neg.
 - A new module BinInt.Pos2Z with results about injections from
   positive to Z
 - A result about Z.pow pushed in the generic layer
 - Zmult_le_compat_{r,l} --> Z.mul_le_mono_nonneg_{r,l}
 - Using tactic Z.le_elim instead of Zle_lt_or_eq
 - Some cleanup in ring, field, micromega
   (use of "Equivalence", "Proper" ...)
 - Some adaptions in QArith (for instance changed Qpower.Qpower_decomp)
 - In ZMake and ZMake, functor parameters are now named NN and ZZ
   instead of N and Z for avoiding confusions

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

1 files changed, 6 insertions, 6 deletions

diff --git a/theories/Logic/EqdepFacts.v b/theories/Logic/EqdepFacts.v
index d84cd8240..4d0560bd7 100644
--- a/theories/Logic/EqdepFacts.v
+++ b/theories/Logic/EqdepFacts.v
@@ -101,7 +101,7 @@ Section Dependent_Equality.
     forall (p q:U) (x:P p) (y:P q), eq_dep p x q y -> eq_dep1 p x q y.
   Proof.
     destruct 1.
-    apply eq_dep1_intro with (refl_equal p).
+    apply eq_dep1_intro with (eq_refl p).
     simpl; trivial.
   Qed.
 
@@ -121,7 +121,7 @@ Proof.
   apply eq_dep_intro.
 Qed.
 
-Notation eq_sigS_eq_dep := eq_sigT_eq_dep (only parsing). (* Compatibility *)
+Notation eq_sigS_eq_dep := eq_sigT_eq_dep (compat "8.2"). (* Compatibility *)
 
 Lemma eq_dep_eq_sigT :
   forall (U:Type) (P:U -> Type) (p q:U) (x:P p) (y:P q),
@@ -250,12 +250,12 @@ Section Equivalences.
   (** Uniqueness of Reflexive Identity Proofs *)
 
   Definition UIP_refl_ :=
-    forall (x:U) (p:x = x), p = refl_equal x.
+    forall (x:U) (p:x = x), p = eq_refl x.
 
   (** Streicher's axiom K *)
 
   Definition Streicher_K_ :=
-    forall (x:U) (P:x = x -> Prop), P (refl_equal x) -> forall p:x = x, P p.
+    forall (x:U) (P:x = x -> Prop), P (eq_refl x) -> forall p:x = x, P p.
 
   (** Injectivity of Dependent Equality is a consequence of *)
   (** Invariance by Substitution of Reflexive Equality Proof *)
@@ -389,14 +389,14 @@ Proof (eq_dep_eq__UIP U eq_dep_eq).
 
 (** Uniqueness of Reflexive Identity Proofs is a direct instance of UIP *)
 
-Lemma UIP_refl : forall (x:U) (p:x = x), p = refl_equal x.
+Lemma UIP_refl : forall (x:U) (p:x = x), p = eq_refl x.
 Proof (UIP__UIP_refl U UIP).
 
 (** Streicher's axiom K is a direct consequence of Uniqueness of
     Reflexive Identity Proofs *)
 
 Lemma Streicher_K :
-  forall (x:U) (P:x = x -> Prop), P (refl_equal x) -> forall p:x = x, P p.
+  forall (x:U) (P:x = x -> Prop), P (eq_refl x) -> forall p:x = x, P p.
 Proof (UIP_refl__Streicher_K U UIP_refl).
 
 End Axioms.