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

4 files changed, 11 insertions, 11 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)