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 /kernel/inductive.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 'kernel/inductive.ml')
| -rw-r--r-- | kernel/inductive.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/kernel/inductive.ml b/kernel/inductive.ml index cd969ea457..320bc6a1cd 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -812,7 +812,7 @@ let rec subterm_specif renv stack t = | Not_subterm -> Not_subterm) | Var _ | Sort _ | Cast _ | Prod _ | LetIn _ | App _ | Const _ | Ind _ - | Construct _ | CoFix _ | Int _ -> Not_subterm + | Construct _ | CoFix _ | Int _ | Float _ -> Not_subterm (* Other terms are not subterms *) @@ -1057,7 +1057,7 @@ let check_one_fix renv recpos trees def = check_rec_call renv stack (Term.applist(c,l)) end - | Sort _ | Int _ -> + | Sort _ | Int _ | Float _ -> assert (List.is_empty l) (* l is not checked because it is considered as the meta's context *) @@ -1254,7 +1254,7 @@ let check_one_cofix env nbfix def deftype = | Evar _ -> List.iter (check_rec_call env alreadygrd n tree vlra) args | Rel _ | Var _ | Sort _ | Cast _ | Prod _ | LetIn _ | App _ | Const _ - | Ind _ | Fix _ | Proj _ | Int _ -> + | Ind _ | Fix _ | Proj _ | Int _ | Float _ -> raise (CoFixGuardError (env,NotGuardedForm t)) in let ((mind, _),_) = codomain_is_coind env deftype in |