diff options
| author | Frédéric Besson | 2020-04-01 11:43:00 +0200 |
|---|---|---|
| committer | Frédéric Besson | 2020-04-01 11:43:00 +0200 |
| commit | 288a97e465048bc47c7d5e91e14bfbc33819e689 (patch) | |
| tree | 1b6afa192518791fe2ae47e3fb4d3033070f4a65 /theories/Reals | |
| parent | 402e37a405e4085365fdcbdc959fe00d2c340da2 (diff) | |
[micromega] use Coqlib.lib_ref to get Coq constants.
Diffstat (limited to 'theories/Reals')
| -rw-r--r-- | theories/Reals/Rregisternames.v | 8 |
1 files changed, 6 insertions, 2 deletions
diff --git a/theories/Reals/Rregisternames.v b/theories/Reals/Rregisternames.v index f09edef600..8b078f2cf3 100644 --- a/theories/Reals/Rregisternames.v +++ b/theories/Reals/Rregisternames.v @@ -8,7 +8,7 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -Require Import Reals. +Require Import Raxioms Rfunctions Qreals. (*****************************************************************) (** Register names for use in plugins *) @@ -18,6 +18,9 @@ Register R as reals.R.type. Register R0 as reals.R.R0. Register R1 as reals.R.R1. Register Rle as reals.R.Rle. +Register Rgt as reals.R.Rgt. +Register Rlt as reals.R.Rlt. +Register Rge as reals.R.Rge. Register Rplus as reals.R.Rplus. Register Ropp as reals.R.Ropp. Register Rminus as reals.R.Rminus. @@ -26,5 +29,6 @@ Register Rinv as reals.R.Rinv. Register Rdiv as reals.R.Rdiv. Register IZR as reals.R.IZR. Register Rabs as reals.R.Rabs. -Register sqrt as reals.R.sqrt. Register powerRZ as reals.R.powerRZ. +Register pow as reals.R.pow. +Register Qreals.Q2R as reals.R.Q2R. |