aboutsummaryrefslogtreecommitdiff
path: root/kernel/vmvalues.mli
diff options
context:
space:
mode:
authorGaëtan Gilbert2020-07-23 11:13:59 +0200
committerGaëtan Gilbert2020-07-23 11:13:59 +0200
commit58df19e952f23ce9376c67f21d09e515a861db0c (patch)
tree8950a7d1a8049a78b00748fd074ab9c5a0c63ddd /kernel/vmvalues.mli
parentb8962b4d7d4c23c01b03713fcd9a0816edad3f40 (diff)
parent675b23dcf824d8a851881171a5628b239aad2201 (diff)
Merge PR #12679: Remove redundant data from VM case switch.
Reviewed-by: SkySkimmer Ack-by: silene
Diffstat (limited to 'kernel/vmvalues.mli')
-rw-r--r--kernel/vmvalues.mli3
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