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 /engine/termops.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 'engine/termops.ml')
| -rw-r--r-- | engine/termops.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/engine/termops.ml b/engine/termops.ml index 2ab2f60421..90fa8546ce 100644 --- a/engine/termops.ml +++ b/engine/termops.ml @@ -600,7 +600,7 @@ let map_constr_with_binders_left_to_right sigma g f l c = let open EConstr in match EConstr.kind sigma c with | (Rel _ | Meta _ | Var _ | Sort _ | Const _ | Ind _ - | Construct _ | Int _) -> c + | Construct _ | Int _ | Float _) -> c | Cast (b,k,t) -> let b' = f l b in let t' = f l t in @@ -681,7 +681,7 @@ let map_constr_with_full_binders_gen userview sigma g f l cstr = let open EConstr in match EConstr.kind sigma cstr with | (Rel _ | Meta _ | Var _ | Sort _ | Const _ | Ind _ - | Construct _ | Int _) -> cstr + | Construct _ | Int _ | Float _) -> cstr | Cast (c,k, t) -> let c' = f l c in let t' = f l t in |