Commit 50641d5d authored by Guillaume Melquiond's avatar Guillaume Melquiond

Rename Definitions.v into Defs.v

parent a999e872
......@@ -2,7 +2,7 @@ FILES = \
Version.v \
Core/Raux.v \
Core/Zaux.v \
Core/Definitions.v \
Core/Defs.v \
Core/Digits.v \
Core/Float_prop.v \
Core/FIX.v \
......
(** * Conditions for innocuous double rounding. *)
Require Import Psatz.
From Flocq Require Import Raux Definitions Generic_fmt Operations Ulp.
From Flocq Require Import Raux Defs Generic_fmt Operations Ulp.
From Flocq Require Import FLX FLT FTZ Double_rounding.
Open Scope R_scope.
......
......@@ -19,7 +19,7 @@ COPYING file for more details.
(** * Locations: where a real number is positioned with respect to its rounded-down value in an arbitrary format. *)
Require Import Raux Definitions Float_prop.
Require Import Raux Defs Float_prop.
Section Fcalc_bracket.
......
......@@ -19,7 +19,7 @@ COPYING file for more details.
(** * Helper function and theorem for computing the rounded quotient of two floating-point numbers. *)
Require Import Raux Definitions Float_prop Digits Bracket.
Require Import Raux Defs Float_prop Digits Bracket.
Section Fcalc_div.
......
......@@ -18,7 +18,7 @@ COPYING file for more details.
*)
(** Basic operations on floats: alignment, addition, multiplication *)
Require Import Raux Definitions Float_prop.
Require Import Raux Defs Float_prop.
Section Float_ops.
......
......@@ -19,7 +19,7 @@ COPYING file for more details.
(** * Helper functions and theorems for computing the rounded square root of a floating-point number. *)
Require Import Raux Definitions Digits Float_prop Bracket.
Require Import Raux Defs Digits Float_prop Bracket.
Section Fcalc_sqrt.
......
......@@ -18,5 +18,5 @@ COPYING file for more details.
*)
(** To ease the import *)
Require Export Raux Definitions Float_prop Round_pred Generic_fmt Round_NE.
Require Export Raux Defs Float_prop Round_pred Generic_fmt Round_NE.
Require Export FIX FLX FLT Ulp.
......@@ -18,7 +18,7 @@ COPYING file for more details.
*)
(** * Fixed-point format *)
Require Import Raux Definitions Round_pred Generic_fmt Ulp Round_NE.
Require Import Raux Defs Round_pred Generic_fmt Ulp Round_NE.
Section RND_FIX.
......
......@@ -18,7 +18,7 @@ COPYING file for more details.
*)
(** * Floating-point format with gradual underflow *)
Require Import Raux Definitions Round_pred Generic_fmt Float_prop.
Require Import Raux Defs Round_pred Generic_fmt Float_prop.
Require Import FLX FIX Ulp Round_NE.
Section RND_FLT.
......
......@@ -18,7 +18,7 @@ COPYING file for more details.
*)
(** * Floating-point format without underflow *)
Require Import Raux Definitions Round_pred Generic_fmt Float_prop.
Require Import Raux Defs Round_pred Generic_fmt Float_prop.
Require Import FIX Ulp Round_NE.
Section RND_FLX.
......
......@@ -18,7 +18,7 @@ COPYING file for more details.
*)
(** * Floating-point format with abrupt underflow *)
Require Import Raux Definitions Round_pred Generic_fmt.
Require Import Raux Defs Round_pred Generic_fmt.
Require Import Float_prop Ulp FLX.
Section RND_FTZ.
......
......@@ -18,7 +18,7 @@ COPYING file for more details.
*)
(** * Basic properties of floating-point formats: lemmas about mantissa, exponent... *)
Require Import Raux Definitions Digits.
Require Import Raux Defs Digits.
Section Float_prop.
......
......@@ -18,7 +18,7 @@ COPYING file for more details.
*)
(** * What is a real number belonging to a format, and many properties. *)
Require Import Raux Definitions Round_pred Float_prop.
Require Import Raux Defs Round_pred Float_prop.
Section Generic.
......
......@@ -18,7 +18,7 @@ COPYING file for more details.
*)
(** * Rounding to nearest, ties to even: existence, unicity... *)
Require Import Raux Definitions Round_pred Generic_fmt Float_prop Ulp.
Require Import Raux Defs Round_pred Generic_fmt Float_prop Ulp.
Notation ZnearestE := (Znearest (fun x => negb (Zeven x))).
......
......@@ -18,7 +18,7 @@ COPYING file for more details.
*)
(** * Roundings: properties and/or functions *)
Require Import Raux Definitions.
Require Import Raux Defs.
Section RND_prop.
......
......@@ -19,7 +19,7 @@ COPYING file for more details.
(** * Unit in the Last Place: our definition using fexp and its properties, successor and predecessor *)
Require Import Reals Psatz.
Require Import Raux Definitions Round_pred Generic_fmt Float_prop.
Require Import Raux Defs Round_pred Generic_fmt Float_prop.
Section Fcore_ulp.
......
(** * Conditions for innocuous double rounding. *)
Require Import Psatz.
Require Import Raux Definitions Generic_fmt Operations Ulp FLX FLT FTZ.
Require Import Raux Defs Generic_fmt Operations Ulp FLX FLT FTZ.
Open Scope R_scope.
......
......@@ -19,7 +19,7 @@ COPYING file for more details.
(** * Error of the rounded-to-nearest addition is representable. *)
Require Import Raux Definitions Float_prop Generic_fmt.
Require Import Raux Defs Float_prop Generic_fmt.
Require Import FIX FLX FLT Ulp Operations.
......
......@@ -19,7 +19,7 @@ COPYING file for more details.
(** * Sterbenz conditions for exact subtraction *)
Require Import Raux Definitions Generic_fmt Operations.
Require Import Raux Defs Generic_fmt Operations.
Section Fprop_Sterbenz.
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment