From f0168fd8ce775b0a96e8cf026e953e9d55f4de25 Mon Sep 17 00:00:00 2001
From: letouzey
Date: Thu, 21 Oct 2010 06:48:00 +0000
Subject: Solve name conflict about pow introduced by commit 13546.

 - NPeano isn't Exported by default anymore (contains pow for nat).
 - in coq_micromega.ml, we specify more where to find the pow of R.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13569 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 plugins/micromega/coq_micromega.ml | 23 ++++++++++++++---------
 1 file changed, 14 insertions(+), 9 deletions(-)

(limited to 'plugins')

diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml
index f3bdebff0a..d410d6a5c8 100644
--- a/plugins/micromega/coq_micromega.ml
+++ b/plugins/micromega/coq_micromega.ml
@@ -220,6 +220,10 @@ struct
       ["Coq";"Reals" ; "Rpow_def"];
       ["LRing_normalise"]]
 
+  let r_modules =
+    [["Coq";"Reals" ; "Rdefinitions"];
+     ["Coq";"Reals" ; "Rpow_def"]]
+
   (**
     * Initialization : a large amount of Caml symbols are derived from
     * ZMicromega.v
@@ -227,6 +231,7 @@ struct
 
   let init_constant = gen_constant_in_modules "ZMicromega" init_modules
   let constant = gen_constant_in_modules "ZMicromega" coq_modules
+  let r_constant = gen_constant_in_modules "ZMicromega" r_modules
   (* let constant = gen_constant_in_modules "Omicron" coq_modules *)
 
   let coq_and = lazy (init_constant "and")
@@ -305,16 +310,16 @@ struct
   let coq_Qmult = lazy (constant "Qmult")
   let coq_Qpower = lazy (constant "Qpower")
 
-  let coq_Rgt = lazy (constant "Rgt")
-  let coq_Rge = lazy (constant "Rge")
-  let coq_Rle = lazy (constant "Rle")
-  let coq_Rlt = lazy (constant "Rlt")
+  let coq_Rgt = lazy (r_constant "Rgt")
+  let coq_Rge = lazy (r_constant "Rge")
+  let coq_Rle = lazy (r_constant "Rle")
+  let coq_Rlt = lazy (r_constant "Rlt")
 
-  let coq_Rplus = lazy (constant "Rplus")
-  let coq_Rminus = lazy (constant "Rminus")
-  let coq_Ropp = lazy (constant "Ropp")
-  let coq_Rmult = lazy (constant "Rmult")
-  let coq_Rpower = lazy (constant "pow")
+  let coq_Rplus = lazy (r_constant "Rplus")
+  let coq_Rminus = lazy (r_constant "Rminus")
+  let coq_Ropp = lazy (r_constant "Ropp")
+  let coq_Rmult = lazy (r_constant "Rmult")
+  let coq_Rpower = lazy (r_constant "pow")
 
   let coq_PEX = lazy (constant "PEX" )
   let coq_PEc = lazy (constant"PEc")
-- 
cgit v1.2.3