mise a jour du nouveau ring et ajout du nouveau field, avant renommages

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

1 files changed, 7 insertions, 7 deletions

diff --git a/theories/Setoids/Setoid.v b/theories/Setoids/Setoid.v
index 884f05e52..b56818629 100644
--- a/theories/Setoids/Setoid.v
+++ b/theories/Setoids/Setoid.v
@@ -82,7 +82,7 @@ Lemma about_carrier_of_relation_class_and_relation_class_of_argument_class :
 
 Inductive nelistT (A : Type) : Type :=
    singl : A -> nelistT A
- | cons : A -> nelistT A -> nelistT A.
+ | necons : A -> nelistT A -> nelistT A.
 
 Definition Arguments := nelistT Argument_Class.
 
@@ -132,7 +132,7 @@ Record Morphism_Theory In Out : Type :=
 Definition list_of_Leibniz_of_list_of_types: nelistT Type -> Arguments.
  induction 1.
    exact (singl (Leibniz _ a)).
-   exact (cons (Leibniz _ a) IHX).
+   exact (necons (Leibniz _ a) IHX).
 Defined.
 
 (* every function is a morphism from Leibniz+ to Leibniz *)
@@ -175,7 +175,7 @@ Defined.
 Definition equality_morphism_of_symmetric_areflexive_transitive_relation:
  forall (A: Type)(Aeq: relation A)(sym: symmetric _ Aeq)(trans: transitive _ Aeq),
   let ASetoidClass := SymmetricAreflexive _ sym in
-   (Morphism_Theory (cons ASetoidClass (singl ASetoidClass)) Iff_Relation_Class).
+   (Morphism_Theory (necons ASetoidClass (singl ASetoidClass)) Iff_Relation_Class).
  intros.
  exists Aeq.
  unfold make_compatibility_goal; simpl; split; eauto.
@@ -184,7 +184,7 @@ Defined.
 Definition equality_morphism_of_symmetric_reflexive_transitive_relation:
  forall (A: Type)(Aeq: relation A)(refl: reflexive _ Aeq)(sym: symmetric _ Aeq)
   (trans: transitive _ Aeq), let ASetoidClass := SymmetricReflexive _ sym refl in
-   (Morphism_Theory (cons ASetoidClass (singl ASetoidClass)) Iff_Relation_Class).
+   (Morphism_Theory (necons ASetoidClass (singl ASetoidClass)) Iff_Relation_Class).
  intros.
  exists Aeq.
  unfold make_compatibility_goal; simpl; split; eauto.
@@ -194,7 +194,7 @@ Definition equality_morphism_of_asymmetric_areflexive_transitive_relation:
  forall (A: Type)(Aeq: relation A)(trans: transitive _ Aeq),
   let ASetoidClass1 := AsymmetricAreflexive Contravariant Aeq in
   let ASetoidClass2 := AsymmetricAreflexive Covariant Aeq in
-   (Morphism_Theory (cons ASetoidClass1 (singl ASetoidClass2)) Impl_Relation_Class).
+   (Morphism_Theory (necons ASetoidClass1 (singl ASetoidClass2)) Impl_Relation_Class).
  intros.
  exists Aeq.
  unfold make_compatibility_goal; simpl; unfold impl; eauto.
@@ -204,7 +204,7 @@ Definition equality_morphism_of_asymmetric_reflexive_transitive_relation:
  forall (A: Type)(Aeq: relation A)(refl: reflexive _ Aeq)(trans: transitive _ Aeq),
   let ASetoidClass1 := AsymmetricReflexive Contravariant refl in
   let ASetoidClass2 := AsymmetricReflexive Covariant refl in
-   (Morphism_Theory (cons ASetoidClass1 (singl ASetoidClass2)) Impl_Relation_Class).
+   (Morphism_Theory (necons ASetoidClass1 (singl ASetoidClass2)) Impl_Relation_Class).
  intros.
  exists Aeq.
  unfold make_compatibility_goal; simpl; unfold impl; eauto.
@@ -331,7 +331,7 @@ with Morphism_Context_List Hole dir :
        check_if_variance_is_respected (variance_of_argument_class S) dir' dir'' ->
         Morphism_Context Hole dir (relation_class_of_argument_class S) dir' ->
          Morphism_Context_List Hole dir dir'' L ->
-          Morphism_Context_List Hole dir dir'' (cons S L).
+          Morphism_Context_List Hole dir dir'' (necons S L).
 
 Scheme Morphism_Context_rect2 := Induction for Morphism_Context  Sort Type
 with Morphism_Context_List_rect2 := Induction for Morphism_Context_List Sort Type.