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 /pretyping/pattern.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 'pretyping/pattern.ml')
| -rw-r--r-- | pretyping/pattern.ml | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/pretyping/pattern.ml b/pretyping/pattern.ml index e0beb383b5..2d7a152817 100644 --- a/pretyping/pattern.ml +++ b/pretyping/pattern.ml @@ -40,6 +40,7 @@ type constr_pattern = | PFix of (int array * int) * (Name.t array * constr_pattern array * constr_pattern array) | PCoFix of int * (Name.t array * constr_pattern array * constr_pattern array) | PInt of Uint63.t + | PFloat of Float64.t (** Nota : in a [PCase], the array of branches might be shorter than expected, denoting the use of a final "_ => _" branch *) |