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

7 files changed, 20 insertions, 20 deletions

diff --git a/contrib/field/Field_Compl.v b/contrib/field/Field_Compl.v
index c90fea1ecc..a5033278c8 100644
--- a/contrib/field/Field_Compl.v
+++ b/contrib/field/Field_Compl.v
@@ -56,6 +56,6 @@ Definition mem :=
          end
      end).
 
-Inductive option (A:Type) : Type :=
-  | None : option A
-  | Some : (A -> A -> A) -> option A.
\ No newline at end of file
+Inductive field_rel_option (A:Type) : Type :=
+  | Field_None : field_rel_option A
+  | Field_Some : (A -> A -> A) -> field_rel_option A.
\ No newline at end of file
diff --git a/contrib/field/Field_Tactic.v b/contrib/field/Field_Tactic.v
index a5b206fb20..245759f6f2 100644
--- a/contrib/field/Field_Tactic.v
+++ b/contrib/field/Field_Tactic.v
@@ -254,11 +254,11 @@ Ltac apply_simplif sfun :=
 
 Ltac unfolds FT :=
   match eval cbv beta iota delta [Aminus] in (Aminus FT) with
-  | (Some _ ?X1) => unfold X1 in |- *
+  | (Field_Some _ ?X1) => unfold X1 in |- *
   | _ => idtac
   end;
    match eval cbv beta iota delta [Adiv] in (Adiv FT) with
-   | (Some _ ?X1) => unfold X1 in |- *
+   | (Field_Some _ ?X1) => unfold X1 in |- *
    | _ => idtac
    end.
 
@@ -304,11 +304,11 @@ Ltac field_gen FT := unfolds FT; (inverse_test FT; ring) || field_gen_aux FT.
 Ltac init_exp FT trm :=
   let e :=
    (match eval cbv beta iota delta [Aminus] in (Aminus FT) with
-    | (Some _ ?X1) => eval cbv beta delta [X1] in trm
+    | (Field_Some _ ?X1) => eval cbv beta delta [X1] in trm
     | _ => trm
     end) in
   match eval cbv beta iota delta [Adiv] in (Adiv FT) with
-  | (Some _ ?X1) => eval cbv beta delta [X1] in e
+  | (Field_Some _ ?X1) => eval cbv beta delta [X1] in e
   | _ => e
   end.
 
diff --git a/contrib/field/Field_Theory.v b/contrib/field/Field_Theory.v
index 35f1125e41..c2739e34a3 100644
--- a/contrib/field/Field_Theory.v
+++ b/contrib/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 : forall n:A, n <> Azero -> Amult (Ainv n) n = Aone}.
 
diff --git a/contrib/field/field.ml4 b/contrib/field/field.ml4
index 76f4b36112..f58bcdd231 100644
--- a/contrib/field/field.ml4
+++ b/contrib/field/field.ml4
@@ -32,8 +32,8 @@ let constant dir s = Coqlib.gen_constant "Field" ("field"::dir) s
 let constr_of_opt a opt =
   let ac = constr_of a in
   match opt with
-  | None -> mkApp ((constant ["Field_Compl"] "None"),[|ac|])
-  | Some f -> mkApp ((constant ["Field_Compl"] "Some"),[|ac;constr_of f|])
+  | None -> mkApp ((constant ["Field_Compl"] "Field_None"),[|ac|])
+  | Some f -> mkApp ((constant ["Field_Compl"] "Field_Some"),[|ac;constr_of f|])
 
 (* Table of theories *)
 let th_tab = ref (Gmap.empty : (constr,constr) Gmap.t)
diff --git a/contrib7/field/Field_Compl.v b/contrib7/field/Field_Compl.v
index aa3a991470..8db3def834 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 cd382bc393..f15e5a4ce5 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 e2710260f9..5af969756a 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
 }.