diff options
| author | Pierre Roux | 2018-08-28 18:56:07 +0200 |
|---|---|---|
| committer | Pierre Roux | 2019-11-01 10:20:35 +0100 |
| commit | d18b928154a48ff8d90aaff69eca7d6eb3dfa0ab (patch) | |
| tree | 9cc9b39b16849ed839f4adf7b19e3d3291f7dd98 /kernel/safe_typing.ml | |
| parent | 79605dabb10e889ae998bf72c8483f095277e693 (diff) | |
Implement classify on primitive float
Diffstat (limited to 'kernel/safe_typing.ml')
| -rw-r--r-- | kernel/safe_typing.ml | 20 |
1 files changed, 20 insertions, 0 deletions
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index 241ee8ada3..d3cffd1546 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -1413,6 +1413,26 @@ let check_register_ind (type t) ind (r : t CPrimitives.prim_ind) env = check_type_cte 2; check_name 3 "FNotComparable"; check_type_cte 3 + | CPrimitives.PIT_f_class -> + check_nconstr 9; + check_name 0 "PNormal"; + check_type_cte 0; + check_name 1 "NNormal"; + check_type_cte 1; + check_name 2 "PSubn"; + check_type_cte 2; + check_name 3 "NSubn"; + check_type_cte 3; + check_name 4 "PZero"; + check_type_cte 4; + check_name 5 "NZero"; + check_type_cte 5; + check_name 6 "PInf"; + check_type_cte 6; + check_name 7 "NInf"; + check_type_cte 7; + check_name 8 "NaN"; + check_type_cte 8 let register_inductive ind prim senv = check_register_ind ind prim senv.env; |