diff options
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; |