diff options
| author | Guillaume Bertholon | 2018-07-13 16:22:35 +0200 |
|---|---|---|
| committer | Pierre Roux | 2019-11-01 10:20:03 +0100 |
| commit | b0b3cc67e01b165272588b2d8bc178840ba83945 (patch) | |
| tree | 0fc62f69eb0b56a3cae6dd81f82ca869dac6fbc9 /interp/notation_term.ml | |
| parent | f93684a412f067622a5026c406bc76032c30b6e9 (diff) | |
Add primitive float computation in Coq kernel
Beware of 0. = -0. issue for primitive floats
The IEEE 754 declares that 0. and -0. are treated equal but we cannot
say that this is true with Leibniz equality.
Therefore we must patch the equality and the total comparison inside the
kernel to prevent inconsistency.
Diffstat (limited to 'interp/notation_term.ml')
| -rw-r--r-- | interp/notation_term.ml | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/interp/notation_term.ml b/interp/notation_term.ml index 908455bd05..c6ddd9ac95 100644 --- a/interp/notation_term.ml +++ b/interp/notation_term.ml @@ -44,6 +44,7 @@ type notation_constr = | NSort of glob_sort | NCast of notation_constr * notation_constr cast_type | NInt of Uint63.t + | NFloat of Float64.t (** Note concerning NList: first constr is iterator, second is terminator; first id is where each argument of the list has to be substituted |