diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-10-26 13:07:34 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-10-26 13:07:34 +0200 |
| commit | 4a82de3b5b9d4a1a0830291b5b9a485bf2a16ded (patch) | |
| tree | 15ff7464cc5a250fbb6ed2a10887d34cfb62a8a4 /kernel/cbytecodes.mli | |
| parent | 95429d01a8f47f5f9d1ecee3b452d920e1e1af22 (diff) | |
| parent | 2290dbb9c95b63e693ced647731623e64297f5c8 (diff) | |
Merge branch 'v8.5' into v8.6
Diffstat (limited to 'kernel/cbytecodes.mli')
| -rw-r--r-- | kernel/cbytecodes.mli | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/kernel/cbytecodes.mli b/kernel/cbytecodes.mli index 5f1f09d00..b8de7619c 100644 --- a/kernel/cbytecodes.mli +++ b/kernel/cbytecodes.mli @@ -39,7 +39,7 @@ val pp_struct_const : structured_constant -> Pp.std_ppcmds type reloc_table = (tag * int) array type annot_switch = - {ci : case_info; rtbl : reloc_table; tailcall : bool} + {ci : case_info; rtbl : reloc_table; tailcall : bool; max_stack_size : int} module Label : sig @@ -84,6 +84,7 @@ type instruction = | Ksequence of bytecodes * bytecodes | Kproj of int * Constant.t (** index of the projected argument, name of projection *) + | Kensurestackcapacity of int (** spiwack: instructions concerning integers *) | Kbranch of Label.t (** jump to label, is it needed ? *) |