diff options
Diffstat (limited to 'kernel/cemitcodes.ml')
| -rw-r--r-- | kernel/cemitcodes.ml | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/kernel/cemitcodes.ml b/kernel/cemitcodes.ml index 277b343b2..1f00a70e7 100644 --- a/kernel/cemitcodes.ml +++ b/kernel/cemitcodes.ml @@ -307,6 +307,8 @@ let init () = type emitcodes = string +let copy = String.copy + let length = String.length type to_patch = emitcodes * (patch list) * fv @@ -348,6 +350,8 @@ let force = force subst_body_code let subst_to_patch_subst = subst_substituted +let repr_body_code = repr_substituted + let to_memory (init_code, fun_code, fv) = init(); emit init_code; |