Renamings to avoid clashes with definitions in Relation_Definitions, now

projections are of the form "equivalence_reflexive" and instance names
too. As they are (almost) never used directly, it does not hurt to have
long explicit names.


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

3 files changed, 43 insertions, 41 deletions

diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4
index 5388bf2073..6b322675c5 100644
--- a/tactics/class_tactics.ml4
+++ b/tactics/class_tactics.ml4
@@ -508,11 +508,11 @@ let coq_relation = lazy (gen_constant ["Relations";"Relation_Definitions"] "rela
 let mk_relation a = mkApp (Lazy.force coq_relation, [| a |])
 let coq_relationT = lazy (gen_constant ["Classes";"Relations"] "relationT")
 
-let setoid_refl_proj = lazy (gen_constant ["Classes"; "SetoidClass"] "equiv_refl")
+let setoid_refl_proj = lazy (gen_constant ["Classes"; "SetoidClass"] "equivalence_reflexive")
 
 let setoid_equiv = lazy (gen_constant ["Classes"; "SetoidClass"] "equiv")
 let setoid_morphism = lazy (gen_constant ["Classes"; "SetoidClass"] "setoid_morphism")
-let setoid_refl_proj = lazy (gen_constant ["Classes"; "SetoidClass"] "equiv_refl")
+let setoid_refl_proj = lazy (gen_constant ["Classes"; "SetoidClass"] "equivalence_reflexive")
   
 let arrow_morphism a b = 
   if isprop a && isprop b then
@@ -1124,17 +1124,17 @@ let init_setoid () =
   check_required_library ["Coq";"Setoids";"Setoid"]
 
 let declare_instance_refl binders a aeq n lemma = 
-  let instance = declare_instance a aeq (add_suffix n "_refl") "Coq.Classes.RelationClasses.Reflexive" 
+  let instance = declare_instance a aeq (add_suffix n "_reflexive") "Coq.Classes.RelationClasses.Reflexive" 
   in anew_instance binders instance 
        [((dummy_loc,id_of_string "reflexivity"),[],lemma)]
 
 let declare_instance_sym binders a aeq n lemma = 
-  let instance = declare_instance a aeq (add_suffix n "_sym") "Coq.Classes.RelationClasses.Symmetric"
+  let instance = declare_instance a aeq (add_suffix n "_symmetric") "Coq.Classes.RelationClasses.Symmetric"
   in anew_instance binders instance 
        [((dummy_loc,id_of_string "symmetry"),[],lemma)]
 
 let declare_instance_trans binders a aeq n lemma = 
-  let instance = declare_instance a aeq (add_suffix n "_trans") "Coq.Classes.RelationClasses.Transitive" 
+  let instance = declare_instance a aeq (add_suffix n "_transitive") "Coq.Classes.RelationClasses.Transitive" 
   in anew_instance binders instance 
        [((dummy_loc,id_of_string "transitivity"),[],lemma)]
 
@@ -1161,16 +1161,16 @@ let declare_relation ?(binders=[]) a aeq n refl symm trans =
 	let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.PreOrder" 
 	in ignore(
 	    anew_instance binders instance 
-	      [((dummy_loc,id_of_string "preorder_refl"), [], mkIdentC lemma_refl);
-	       ((dummy_loc,id_of_string "preorder_trans"),[], mkIdentC lemma_trans)])
+	      [((dummy_loc,id_of_string "preorder_reflexive"), [], mkIdentC lemma_refl);
+	       ((dummy_loc,id_of_string "preorder_transitive"),[], mkIdentC lemma_trans)])
     | (None, Some lemma2, Some lemma3) -> 
 	let lemma_sym = declare_instance_sym binders a aeq n lemma2 in
 	let lemma_trans = declare_instance_trans binders a aeq n lemma3 in
 	let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.PER" 
 	in ignore(
 	    anew_instance binders instance 
-	      [((dummy_loc,id_of_string "per_sym"),  [], mkIdentC lemma_sym);
-	       ((dummy_loc,id_of_string "per_trans"),[], mkIdentC lemma_trans)])
+	      [((dummy_loc,id_of_string "per_symmetric"),  [], mkIdentC lemma_sym);
+	       ((dummy_loc,id_of_string "per_transitive"),[], mkIdentC lemma_trans)])
      | (Some lemma1, Some lemma2, Some lemma3) -> 
 	let lemma_refl = declare_instance_refl binders a aeq n lemma1 in 
 	let lemma_sym = declare_instance_sym binders a aeq n lemma2 in
@@ -1178,9 +1178,9 @@ let declare_relation ?(binders=[]) a aeq n refl symm trans =
 	let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.Equivalence" 
 	in ignore(
 	  anew_instance binders instance 
-	    [((dummy_loc,id_of_string "equiv_refl"), [], mkIdentC lemma_refl);
-	     ((dummy_loc,id_of_string "equiv_sym"),  [], mkIdentC lemma_sym);
-	     ((dummy_loc,id_of_string "equiv_trans"),[], mkIdentC lemma_trans)])
+	    [((dummy_loc,id_of_string "equivalence_reflexive"), [], mkIdentC lemma_refl);
+	     ((dummy_loc,id_of_string "equivalence_symmetric"),  [], mkIdentC lemma_sym);
+	     ((dummy_loc,id_of_string "equivalence_transitive"),[], mkIdentC lemma_trans)])
 
 type 'a binders_let_argtype = (local_binder list, 'a) Genarg.abstract_argument_type
 
@@ -1355,9 +1355,9 @@ let add_setoid binders a aeq t n =
   let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.Equivalence"
   in ignore(
     anew_instance binders instance
-      [((dummy_loc,id_of_string "equiv_refl"), [], mkIdentC lemma_refl);
-       ((dummy_loc,id_of_string "equiv_sym"),  [], mkIdentC lemma_sym);
-       ((dummy_loc,id_of_string "equiv_trans"),[], mkIdentC lemma_trans)])
+      [((dummy_loc,id_of_string "equivalence_reflexive"), [], mkIdentC lemma_refl);
+       ((dummy_loc,id_of_string "equivalence_symmetric"),  [], mkIdentC lemma_sym);
+       ((dummy_loc,id_of_string "equivalence_transitive"),[], mkIdentC lemma_trans)])
 
 let add_morphism_infer m n =
   init_setoid ();
diff --git a/theories/Classes/Equivalence.v b/theories/Classes/Equivalence.v
index d7774a2d77..f40d2e2a5e 100644
--- a/theories/Classes/Equivalence.v
+++ b/theories/Classes/Equivalence.v
@@ -37,23 +37,25 @@ Definition equiv [ Equivalence A R ] : relation A := R.
 
 Typeclasses unfold @equiv.
 
+
+
 (* (** Shortcuts to make proof search possible (unification won't unfold equiv). *) *)
 
-(* Program Instance [ sa : Equivalence A ] => equiv_refl : Reflexive equiv. *)
+Program Instance [ sa : Equivalence A ] => equiv_refl : Reflexive equiv.
 
-(* Program Instance [ sa : Equivalence A ] => equiv_sym : Symmetric equiv. *)
+Program Instance [ sa : Equivalence A ] => equiv_sym : Symmetric equiv.
 
-(*   Next Obligation. *)
-(*   Proof. *)
-(*     symmetry ; auto. *)
-(*   Qed. *)
+  Next Obligation.
+  Proof.
+    symmetry ; auto.
+  Qed.
 
-(* Program Instance [ sa : Equivalence A ] => equiv_trans : Transitive equiv. *)
+Program Instance [ sa : Equivalence A ] => equiv_trans : Transitive equiv.
 
-(*   Next Obligation. *)
-(*   Proof. *)
-(*     transitivity y ; auto. *)
-(*   Qed. *)
+  Next Obligation.
+  Proof.
+    transitivity y ; auto.
+  Qed.
 
 (** Overloaded notations for setoid equivalence and inequivalence. Not to be confused with [eq] and [=]. *)
 
diff --git a/theories/Classes/RelationClasses.v b/theories/Classes/RelationClasses.v
index ef3cba81f1..ebbd887c2a 100644
--- a/theories/Classes/RelationClasses.v
+++ b/theories/Classes/RelationClasses.v
@@ -141,34 +141,34 @@ Ltac obligations_tactic ::= simpl_relation.
 
 (** Logical implication. *)
 
-Program Instance impl_refl : Reflexive impl.
-Program Instance impl_trans : Transitive impl.
+Program Instance impl_reflexive : Reflexive impl.
+Program Instance impl_transitive : 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_reflexive : Reflexive iff.
+Program Instance iff_symmetric : Symmetric iff.
+Program Instance iff_transitive : 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_reflexive : Reflexive (@eq A).
+Program Instance eq_symmetric : Symmetric (@eq A).
+Program Instance eq_transitive : Transitive (@eq A).
 
 (** Various combinations of reflexivity, symmetry and transitivity. *)
 
 (** A [PreOrder] is both Reflexive and Transitive. *)
 
 Class PreOrder A (R : relation A) :=
-  preorder_refl :> Reflexive R ;
-  preorder_trans :> Transitive R.
+  preorder_reflexive :> Reflexive R ;
+  preorder_transitive :> Transitive R.
 
 (** A partial equivalence relation is Symmetric and Transitive. *)
 
 Class PER (carrier : Type) (pequiv : relation carrier) :=
-  per_sym :> Symmetric pequiv ;
-  per_trans :> Transitive pequiv.
+  per_symmetric :> Symmetric pequiv ;
+  per_transitive :> Transitive pequiv.
 
 (** We can build a PER on the Coq function space if we have PERs on the domain and
    codomain. *)
@@ -187,9 +187,9 @@ Program Instance [ PER A (R : relation A), PER B (R' : relation B) ] =>
 (** The [Equivalence] typeclass. *)
 
 Class Equivalence (carrier : Type) (equiv : relation carrier) :=
-  equiv_refl :> Reflexive equiv ;
-  equiv_sym :> Symmetric equiv ;
-  equiv_trans :> Transitive equiv.
+  equivalence_reflexive :> Reflexive equiv ;
+  equivalence_symmetric :> Symmetric equiv ;
+  equivalence_transitive :> Transitive equiv.
 
 (** We can now define antisymmetry w.r.t. an equivalence relation on the carrier. *)