reals: renamed type option into field_rel_option

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

3 files changed, 9 insertions, 9 deletions

diff --git a/contrib7/field/Field_Compl.v b/contrib7/field/Field_Compl.v
index aa3a99147..8db3def83 100644
--- a/contrib7/field/Field_Compl.v
+++ b/contrib7/field/Field_Compl.v
@@ -57,6 +57,6 @@ Fix mem {mem [A:Set;eq_dec:(e1,e2:A){e1=e2}+{~e1=e2};a:A;l:(listT A)] : bool :=
     end
   end}.
 
-Inductive option [A:Type] : Type :=
-  | None : (option A)
-  | Some : (A -> A -> A) -> (option A).
+Inductive field_rel_option [A:Type] : Type :=
+  | Field_None : (field_rel_option A)
+  | Field_Some : (A -> A -> A) -> (field_rel_option A).
diff --git a/contrib7/field/Field_Tactic.v b/contrib7/field/Field_Tactic.v
index cd382bc39..f15e5a4ce 100644
--- a/contrib7/field/Field_Tactic.v
+++ b/contrib7/field/Field_Tactic.v
@@ -236,10 +236,10 @@ Tactic Definition ApplySimplif sfun :=
 
 Tactic Definition Unfolds FT :=
   (Match Eval Cbv Beta Delta [Aminus] Iota in (Aminus FT) With
-   | [(Some ? ?1)] -> Unfold ?1
+   | [(Field_Some ? ?1)] -> Unfold ?1
    | _ -> Idtac);
   (Match Eval Cbv Beta Delta [Adiv] Iota in (Adiv FT) With
-   | [(Some ? ?1)] -> Unfold ?1
+   | [(Field_Some ? ?1)] -> Unfold ?1
    | _ -> Idtac).
 
 Tactic Definition Reduce FT :=
@@ -281,10 +281,10 @@ V7only [Tactic Definition field_gen := Field_Gen.].
 Meta Definition InitExp FT trm :=
   Let e =
     (Match Eval Cbv Beta Delta [Aminus] Iota in (Aminus FT) With
-     | [(Some ? ?1)] -> Eval Cbv Beta Delta [?1] in trm
+     | [(Field_Some ? ?1)] -> Eval Cbv Beta Delta [?1] in trm
      | _ -> trm) In
   Match Eval Cbv Beta Delta [Adiv] Iota in (Adiv FT) With
-  | [(Some ? ?1)] -> Eval Cbv Beta Delta [?1] in e
+  | [(Field_Some ? ?1)] -> Eval Cbv Beta Delta [?1] in e
   | _ -> e.
 V7only [
 (*Used by contrib Maple *)
diff --git a/contrib7/field/Field_Theory.v b/contrib7/field/Field_Theory.v
index e2710260f..5af969756 100644
--- a/contrib7/field/Field_Theory.v
+++ b/contrib7/field/Field_Theory.v
@@ -21,8 +21,8 @@ Record Field_Theory : Type :=
   Aopp : A -> A;
   Aeq : A -> A -> bool;
   Ainv : A -> A;
-  Aminus : (option A);
-  Adiv : (option A);
+  Aminus : (field_rel_option A);
+  Adiv : (field_rel_option A);
   RT : (Ring_Theory Aplus Amult Aone Azero Aopp Aeq);
   Th_inv_def : (n:A)~(n=Azero)->(Amult (Ainv n) n)=Aone
 }.