diff options
| author |  Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2016-12-16 17:23:33 +0100 |
|---|---|---|
| committer |  Maxime Dénès <mail@maximedenes.fr> | 2017-03-22 16:29:33 +0100 |
| commit | d2061bd8cd2d809d6e5a849dd150e9e0d74331fc (patch) | |
| tree | ae840147edccf890fa3531487619adc87c2631c4 /plugins/micromega/coq_micromega.ml | |
| parent | 8b73fd7c6ce423f8c8a2594e90200f2407795d52 (diff) | |
Remove duplicate lemmas.
Diffstat (limited to 'plugins/micromega/coq_micromega.ml')
| -rw-r--r-- | plugins/micromega/coq_micromega.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml index 97f29df82..6051cb3d3 100644 --- a/plugins/micromega/coq_micromega.ml +++ b/plugins/micromega/coq_micromega.ml @@ -364,6 +364,7 @@ struct [["Coq";"Reals" ; "Rdefinitions"]; ["Coq";"Reals" ; "Rpow_def"] ; ["Coq";"Reals" ; "Raxioms"] ; + ["Coq";"QArith"; "Qreals"] ; ] let z_modules = [["Coq";"ZArith";"BinInt"]] @@ -479,7 +480,7 @@ struct let coq_Rinv = lazy (r_constant "Rinv") let coq_Rpower = lazy (r_constant "pow") let coq_IZR = lazy (r_constant "IZR") - let coq_IQR = lazy (constant "IQR") + let coq_IQR = lazy (r_constant "Q2R") let coq_PEX = lazy (constant "PEX" ) |