diff options
| author | Pierre-Marie Pédrot | 2020-05-14 13:58:23 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-07-22 12:46:20 +0200 |
| commit | 675b23dcf824d8a851881171a5628b239aad2201 (patch) | |
| tree | 90b800d6524b93c23c0adc6e0a941db7f421cc79 /kernel/vmvalues.mli | |
| parent | e6d92a9765f84c80f8c6a102fe5480490c747313 (diff) | |
Remove redundant data from VM case switch.
No need to store the case_info, all the data is reconstructible from the
context. Furthermore, this reconstruction is performed in a context where
we already access the environment, so performance is not at stake.
Hopefully this will also reduce the number of globally allocated VM values,
since the switch representation now only depends on the shape of the inductive
type.
Diffstat (limited to 'kernel/vmvalues.mli')
| -rw-r--r-- | kernel/vmvalues.mli | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/kernel/vmvalues.mli b/kernel/vmvalues.mli index f4070a02a3..f6efd49cfc 100644 --- a/kernel/vmvalues.mli +++ b/kernel/vmvalues.mli @@ -9,7 +9,6 @@ (************************************************************************) open Names -open Constr (** Values *) @@ -52,7 +51,7 @@ val pp_struct_const : structured_constant -> Pp.t type reloc_table = (tag * int) array type annot_switch = - {ci : case_info; rtbl : reloc_table; tailcall : bool; max_stack_size : int} + { rtbl : reloc_table; tailcall : bool; max_stack_size : int } val eq_structured_constant : structured_constant -> structured_constant -> bool val hash_structured_constant : structured_constant -> int |