bugfix micromega: solved an ambiguous symbol resolution

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

1 files changed, 18 insertions, 14 deletions

diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml
index 082814655c..77d2d9ac85 100644
--- a/plugins/micromega/coq_micromega.ml
+++ b/plugins/micromega/coq_micromega.ml
@@ -276,10 +276,10 @@ struct
     *)
 
   let logic_dir = ["Coq";"Logic";"Decidable"]
-  let coq_modules =
-   init_modules @
-    [logic_dir] @ arith_modules @ zarith_base_modules @
-    [ ["Coq";"Lists";"List"];
+
+  let mic_modules = 
+    [ 
+      ["Coq";"Lists";"List"];
       ["ZMicromega"];
       ["Tauto"];
       ["RingMicromega"];
@@ -294,6 +294,10 @@ struct
       ["Coq";"Reals" ; "Rpow_def"];
       ["LRing_normalise"]]
 
+  let coq_modules =
+   init_modules @
+    [logic_dir] @ arith_modules @ zarith_base_modules @ mic_modules
+
   let bin_module = [["Coq";"Numbers";"BinNums"]]
 
   let r_modules =
@@ -313,7 +317,7 @@ struct
   let bin_constant = gen_constant_in_modules "ZMicromega" bin_module
   let r_constant = gen_constant_in_modules "ZMicromega" r_modules
   let z_constant = gen_constant_in_modules "ZMicromega" z_modules
-  (* let constant = gen_constant_in_modules "Omicron" coq_modules *)
+  let m_constant = gen_constant_in_modules "ZMicromega" mic_modules
 
   let coq_and = lazy (init_constant "and")
   let coq_or = lazy (init_constant "or")
@@ -355,15 +359,15 @@ struct
   let coq_Qmake = lazy (constant "Qmake")
 
   let coq_Rcst = lazy (constant "Rcst")
-  let coq_C0   = lazy (constant "C0")
-  let coq_C1   = lazy (constant "C1")
-  let coq_CQ   = lazy (constant "CQ")
-  let coq_CZ   = lazy (constant "CZ")
-  let coq_CPlus = lazy (constant "CPlus")
-  let coq_CMinus = lazy (constant "CMinus")
-  let coq_CMult  = lazy (constant "CMult")
-  let coq_CInv   = lazy (constant "CInv")
-  let coq_COpp   = lazy (constant "COpp")
+  let coq_C0   = lazy (m_constant "C0")
+  let coq_C1   = lazy (m_constant "C1")
+  let coq_CQ   = lazy (m_constant "CQ")
+  let coq_CZ   = lazy (m_constant "CZ")
+  let coq_CPlus = lazy (m_constant "CPlus")
+  let coq_CMinus = lazy (m_constant "CMinus")
+  let coq_CMult  = lazy (m_constant "CMult")
+  let coq_CInv   = lazy (m_constant "CInv")
+  let coq_COpp   = lazy (m_constant "COpp")
 
 
   let coq_R0    = lazy (constant "R0")