diff options
Diffstat (limited to 'checker/values.ml')
| -rw-r--r-- | checker/values.ml | 14 |
1 files changed, 9 insertions, 5 deletions
diff --git a/checker/values.ml b/checker/values.ml index 9a2028a96b..56321a27ff 100644 --- a/checker/values.ml +++ b/checker/values.ml @@ -35,6 +35,7 @@ type value = | Proxy of value ref | Uint63 + | Float64 let fix (f : value -> value) : value = let self = ref Any in @@ -116,7 +117,7 @@ let v_binder_annot x = v_tuple "binder_annot" [|x;v_relevance|] let v_puniverses v = v_tuple "punivs" [|v;v_instance|] -let v_boollist = List v_bool +let v_boollist = List v_bool let v_caseinfo = let v_cstyle = v_enum "case_style" 5 in @@ -147,7 +148,8 @@ let rec v_constr = [|v_fix|]; (* Fix *) [|v_cofix|]; (* CoFix *) [|v_proj;v_constr|]; (* Proj *) - [|Uint63|] (* Int *) + [|Uint63|]; (* Int *) + [|Float64|] (* Int *) |]) and v_prec = Tuple ("prec_declaration", @@ -226,7 +228,7 @@ let v_pol_arity = v_tuple "polymorphic_arity" [|List(Opt v_level);v_univ|] let v_primitive = - v_enum "primitive" 25 + v_enum "primitive" 44 (* Number of "Primitive" in Int63.v and PrimFloat.v *) let v_cst_def = v_sum "constant_def" 0 @@ -300,9 +302,11 @@ let v_ind_pack = v_tuple "mutual_inductive_body" Opt v_bool; v_typing_flags|] -let v_prim_ind = v_enum "prim_ind" 4 +let v_prim_ind = v_enum "prim_ind" 6 +(* Number of "Register ... as kernel.ind_..." in Int63.v and PrimFloat.v *) -let v_prim_type = v_enum "prim_type" 1 +let v_prim_type = v_enum "prim_type" 2 +(* Number of constructors of prim_type in "kernel/cPrimitives.ml" *) let v_retro_action = v_sum "retro_action" 0 [| |