Skip to content
Snippets Groups Projects
Commit 0a6c8b8e authored by Allan Blanchard's avatar Allan Blanchard
Browse files

[wp] Removes unused elements in Cfloat.mlw

parent c3dbc9a7
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
src/plugins/wp/share/why3/frama_c_wp/cfloat.mlw
+ 0
− 6
View file @ 0a6c8b8e
...@@ -28,7 +28,6 @@ theory Cfloat ...@@ -28,7 +28,6 @@ theory Cfloat
use real.Abs use real.Abs
use ieee_float.RoundingMode as Rounding use ieee_float.RoundingMode as Rounding
use ieee_float.GenericFloat as Generic
use ieee_float.Float32 as F32 use ieee_float.Float32 as F32
use ieee_float.Float64 as F64 use ieee_float.Float64 as F64
use real.RealInfix use real.RealInfix
...@@ -42,14 +41,9 @@ theory Cfloat ...@@ -42,14 +41,9 @@ theory Cfloat
(* C-Float Conversion *) (* C-Float Conversion *)
function of_f32 (f: f32) : real = F32.t'real f function of_f32 (f: f32) : real = F32.t'real f
function of_f64 (d: f64) : real = F64.t'real d function of_f64 (d: f64) : real = F64.t'real d
(* C-Float Rounding Modes *)
type rounding_mode = Rounding.mode
(* C-Float Classification *) (* C-Float Classification *)
predicate is_finite_f32 (f:f32) = F32.t'isFinite f predicate is_finite_f32 (f:f32) = F32.t'isFinite f
......
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