diff options
| author | Maxime Dénès | 2018-02-19 10:12:22 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2018-02-19 10:12:22 +0100 |
| commit | c047ecce6e4dba33df69a53a9e168999676c65db (patch) | |
| tree | 83fb92feaff7904a2f091a7c510aae1e3f766a5d /kernel/cemitcodes.mli | |
| parent | 9accca23fb79f8a14d1cd35fa681a2e0bece1db5 (diff) | |
| parent | 745696124240963616a38f41b1a20f199646c5dc (diff) | |
Merge PR #6230: Better Cemitcodes API + compact relocation representation
Diffstat (limited to 'kernel/cemitcodes.mli')
| -rw-r--r-- | kernel/cemitcodes.mli | 14 |
1 files changed, 3 insertions, 11 deletions
diff --git a/kernel/cemitcodes.mli b/kernel/cemitcodes.mli index fee45aafd8..03920dc1a3 100644 --- a/kernel/cemitcodes.mli +++ b/kernel/cemitcodes.mli @@ -6,20 +6,12 @@ type reloc_info = | Reloc_const of structured_constant | Reloc_getglobal of Constant.t -type patch = reloc_info * int - -(* A virer *) -val subst_patch : Mod_subst.substitution -> patch -> patch - +type patches type emitcodes -val length : emitcodes -> int - -val patch_int : emitcodes -> ((*pos*)int * int) list -> emitcodes - -type to_patch = emitcodes * (patch list) * fv +val patch : emitcodes -> patches -> (reloc_info -> int) -> Vmvalues.tcode -val subst_to_patch : Mod_subst.substitution -> to_patch -> to_patch +type to_patch = emitcodes * patches * fv type body_code = | BCdefined of to_patch |