Switched to "standardized" names for the properties of eq and

identity. Add notations for compatibility and support for
understanding these notations in the ml files.



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

4 files changed, 38 insertions, 28 deletions

diff --git a/theories/FSets/FSetFullAVL.v b/theories/FSets/FSetFullAVL.v
index ac8800923..64d5eb8af 100644
--- a/theories/FSets/FSetFullAVL.v
+++ b/theories/FSets/FSetFullAVL.v
@@ -522,8 +522,6 @@ Ltac ocaml_union_tac :=
   rewrite H; simpl; romega with *
  end.
 
-Import Logic. (* Unhide eq, otherwise Function complains. *)
-
 Function ocaml_union (s : t * t) { measure cardinal2 s } : t  :=
  match s with 
   | (Leaf, Leaf) => s#2
diff --git a/theories/Init/Datatypes.v b/theories/Init/Datatypes.v
index cb96f3f60..73e4924aa 100644
--- a/theories/Init/Datatypes.v
+++ b/theories/Init/Datatypes.v
@@ -114,8 +114,8 @@ Inductive Empty_set : Set :=.
     sole inhabitant is denoted [refl_identity A a] *)
 
 Inductive identity (A:Type) (a:A) : A -> Type :=
-  refl_identity : identity (A:=A) a a.
-Hint Resolve refl_identity: core.
+  identity_refl : identity a a.
+Hint Resolve identity_refl: core.
 
 Implicit Arguments identity_ind [A].
 Implicit Arguments identity_rec [A].
diff --git a/theories/Init/Logic.v b/theories/Init/Logic.v
index a91fd0480..ede73ebf1 100644
--- a/theories/Init/Logic.v
+++ b/theories/Init/Logic.v
@@ -243,7 +243,7 @@ End universal_quantification.
     [A] which is true of [x] is also true of [y] *)
 
 Inductive eq (A:Type) (x:A) : A -> Prop :=
-    refl_equal : x = x :>A
+    eq_refl : x = x :>A
 
 where "x = y :> A" := (@eq A x y) : type_scope.
 
@@ -255,7 +255,7 @@ Implicit Arguments eq_ind [A].
 Implicit Arguments eq_rec [A].
 Implicit Arguments eq_rect [A].
 
-Hint Resolve I conj or_introl or_intror refl_equal: core.
+Hint Resolve I conj or_introl or_intror eq_refl: core.
 Hint Resolve ex_intro ex_intro2: core.
 
 Section Logic_lemmas.
@@ -271,17 +271,17 @@ Section Logic_lemmas.
     Variable f : A -> B.
     Variables x y z : A.
 
-    Theorem sym_eq : x = y -> y = x.
+    Theorem eq_sym : x = y -> y = x.
     Proof.
       destruct 1; trivial.
     Defined.
-    Opaque sym_eq.
+    Opaque eq_sym.
 
-    Theorem trans_eq : x = y -> y = z -> x = z.
+    Theorem eq_trans : x = y -> y = z -> x = z.
     Proof.
       destruct 2; trivial.
     Defined.
-    Opaque trans_eq.
+    Opaque eq_trans.
 
     Theorem f_equal : x = y -> f x = f y.
     Proof.
@@ -289,30 +289,26 @@ Section Logic_lemmas.
     Defined.
     Opaque f_equal.
 
-    Theorem sym_not_eq : x <> y -> y <> x.
+    Theorem not_eq_sym : x <> y -> y <> x.
     Proof.
       red in |- *; intros h1 h2; apply h1; destruct h2; trivial.
     Qed.
 
-    Definition sym_equal := sym_eq.
-    Definition sym_not_equal := sym_not_eq.
-    Definition trans_equal := trans_eq.
-
   End equality.
 
   Definition eq_ind_r :
     forall (A:Type) (x:A) (P:A -> Prop), P x -> forall y:A, y = x -> P y.
-    intros A x P H y H0; elim sym_eq with (1 := H0); assumption.
+    intros A x P H y H0; elim eq_sym with (1 := H0); assumption.
   Defined.
 
   Definition eq_rec_r :
     forall (A:Type) (x:A) (P:A -> Set), P x -> forall y:A, y = x -> P y.
-    intros A x P H y H0; elim sym_eq with (1 := H0); assumption.
+    intros A x P H y H0; elim eq_sym with (1 := H0); assumption.
   Defined.
 
   Definition eq_rect_r :
     forall (A:Type) (x:A) (P:A -> Type), P x -> forall y:A, y = x -> P y.
-    intros A x P H y H0; elim sym_eq with (1 := H0); assumption.
+    intros A x P H y H0; elim eq_sym with (1 := H0); assumption.
   Defined.
 End Logic_lemmas.
 
@@ -349,7 +345,18 @@ Proof.
   destruct 1; destruct 1; destruct 1; destruct 1; destruct 1; reflexivity.
 Qed.
 
-Hint Immediate sym_eq sym_not_eq: core.
+(* Aliases *)
+
+Notation sym_eq := eq_sym (only parsing).
+Notation trans_eq := eq_trans (only parsing).
+Notation sym_not_eq := not_eq_sym (only parsing).
+
+Notation refl_equal := eq_refl (only parsing).
+Notation sym_equal := eq_sym (only parsing).
+Notation trans_equal := eq_trans (only parsing).
+Notation sym_not_equal := not_eq_sym (only parsing).
+
+Hint Immediate eq_sym not_eq_sym: core.
 
 (** Basic definitions about relations and properties *)
 
@@ -411,7 +418,7 @@ intros A x y z H1 H2. rewrite <- H2; exact H1.
 Qed.
 
 Declare Left Step eq_stepl.
-Declare Right Step trans_eq.
+Declare Right Step eq_trans.
 
 Lemma iff_stepl : forall A B C : Prop, (A <-> B) -> (A <-> C) -> (C <-> B).
 Proof.
diff --git a/theories/Init/Logic_Type.v b/theories/Init/Logic_Type.v
index f5cee92c7..bdec651da 100644
--- a/theories/Init/Logic_Type.v
+++ b/theories/Init/Logic_Type.v
@@ -29,22 +29,22 @@ Section identity_is_a_congruence.
 
  Variables x y z : A.
  
- Lemma sym_id : identity x y -> identity y x.
+ Lemma identity_sym : identity x y -> identity y x.
  Proof.
   destruct 1; trivial.
  Defined.
 
- Lemma trans_id : identity x y -> identity y z -> identity x z.
+ Lemma identity_trans : identity x y -> identity y z -> identity x z.
  Proof.
   destruct 2; trivial.
  Defined.
 
- Lemma congr_id : identity x y -> identity (f x) (f y).
+ Lemma identity_congr : identity x y -> identity (f x) (f y).
  Proof.
   destruct 1; trivial.
  Defined.
 
- Lemma sym_not_id : notT (identity x y) -> notT (identity y x).
+ Lemma not_identity_sym : notT (identity x y) -> notT (identity y x).
  Proof.
   red in |- *; intros H H'; apply H; destruct H'; trivial.
  Qed.
@@ -53,17 +53,22 @@ End identity_is_a_congruence.
 
 Definition identity_ind_r :
   forall (A:Type) (a:A) (P:A -> Prop), P a -> forall y:A, identity y a -> P y.
- intros A x P H y H0; case sym_id with (1 := H0); trivial.
+ intros A x P H y H0; case identity_sym with (1 := H0); trivial.
 Defined.
 
 Definition identity_rec_r :
   forall (A:Type) (a:A) (P:A -> Set), P a -> forall y:A, identity y a -> P y.
- intros A x P H y H0; case sym_id with (1 := H0); trivial.
+ intros A x P H y H0; case identity_sym with (1 := H0); trivial.
 Defined.
 
 Definition identity_rect_r :
   forall (A:Type) (a:A) (P:A -> Type), P a -> forall y:A, identity y a -> P y.
- intros A x P H y H0; case sym_id with (1 := H0); trivial.
+ intros A x P H y H0; case identity_sym with (1 := H0); trivial.
 Defined.
 
-Hint Immediate sym_id sym_not_id: core v62.
+Hint Immediate identity_sym not_identity_sym: core v62.
+
+Notation refl_id := identity_refl (only parsing).
+Notation sym_id := identity_sym (only parsing).
+Notation trans_id := identity_trans (only parsing).
+Notation sym_not_id := not_identity_sym (only parsing).