diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-10-21 06:48:00 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-10-21 06:48:00 +0000 |
| commit | f0168fd8ce775b0a96e8cf026e953e9d55f4de25 (patch) | |
| tree | edbca2c262da236a72bfe5db54b7f700eb17d430 /plugins/micromega | |
| parent | 843bbc240d6ece54efc4f6f13035ef0ffac8f886 (diff) | |
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
Diffstat (limited to 'plugins/micromega')
| -rw-r--r-- | plugins/micromega/coq_micromega.ml | 23 |
1 files changed, 14 insertions, 9 deletions
diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml index f3bdebff0..d410d6a5c 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") |