diff options
| -rw-r--r-- | plugins/micromega/coq_micromega.ml | 23 | ||||
| -rw-r--r-- | theories/Arith/Max.v | 2 | ||||
| -rw-r--r-- | theories/Arith/Min.v | 2 | ||||
| -rw-r--r-- | theories/Reals/Rtrigo_def.v | 2 |
4 files changed, 17 insertions, 12 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") diff --git a/theories/Arith/Max.v b/theories/Arith/Max.v index 2022331bb..77dfa5080 100644 --- a/theories/Arith/Max.v +++ b/theories/Arith/Max.v @@ -8,7 +8,7 @@ (** THIS FILE IS DEPRECATED. Use [NPeano.Nat] instead. *) -Require Export NPeano. +Require Import NPeano. Local Open Scope nat_scope. Implicit Types m n p : nat. diff --git a/theories/Arith/Min.v b/theories/Arith/Min.v index 742c8126c..2b2cf860d 100644 --- a/theories/Arith/Min.v +++ b/theories/Arith/Min.v @@ -8,7 +8,7 @@ (** THIS FILE IS DEPRECATED. Use [NPeano.Nat] instead. *) -Require Export NPeano. +Require Import NPeano. Open Local Scope nat_scope. Implicit Types m n p : nat. diff --git a/theories/Reals/Rtrigo_def.v b/theories/Reals/Rtrigo_def.v index 27393c265..c64931353 100644 --- a/theories/Reals/Rtrigo_def.v +++ b/theories/Reals/Rtrigo_def.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -Require Import Max Rbase Rfunctions SeqSeries Rtrigo_fun. +Require Import Rbase Rfunctions SeqSeries Rtrigo_fun Max. Open Local Scope R_scope. (********************************) |