Commit 1b8f4e70 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Substitute all the constants (fix issue #110).

parent 188a89ac
......@@ -617,6 +617,7 @@ module SingleFull
clone export GenFloatSpecFull with
type t = single,
constant min = min_single,
constant max = max_single,
constant max_representable_integer = max_int,
lemma Bounded_real_no_overflow
......@@ -633,6 +634,7 @@ module DoubleFull
clone export GenFloatSpecFull with
type t = double,
constant min = min_double,
constant max = max_double,
constant max_representable_integer = max_int,
lemma Bounded_real_no_overflow
......
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