diff options
| author | Pierre Roux | 2019-02-20 18:00:04 +0100 |
|---|---|---|
| committer | Pierre Roux | 2019-11-01 10:20:51 +0100 |
| commit | 6133877fc097412233a60740fdf94374abb79559 (patch) | |
| tree | 26655b276f177cc77f108524278eb620e03c97c1 /checker/values.ml | |
| parent | f0bf1511e59e528e090a87cfcc220f93c2431ecd (diff) | |
Add primitive floats to checker
Diffstat (limited to 'checker/values.ml')
| -rw-r--r-- | checker/values.ml | 12 |
1 files changed, 8 insertions, 4 deletions
diff --git a/checker/values.ml b/checker/values.ml index 9a2028a96b..0cd63566d7 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 @@ -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" 41 (* 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 [| |