blob: 8117d975fe563102240f3bd207b49af23c567bba (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
|
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
(* v * Copyright INRIA, CNRS and contributors *)
(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
Require Import Raxioms Rfunctions.
(*****************************************************************)
(** Register names for use in plugins *)
(*****************************************************************)
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.
Register Rmult as reals.R.Rmult.
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 powerRZ as reals.R.powerRZ.
Register pow as reals.R.pow.
Register Q2R as reals.R.Q2R.
|
