summaryrefslogtreecommitdiff
path: root/kernel/cbytegen.mli
diff options
context:
space:
mode:
Diffstat (limited to 'kernel/cbytegen.mli')
-rw-r--r--kernel/cbytegen.mli13
1 files changed, 7 insertions, 6 deletions
diff --git a/kernel/cbytegen.mli b/kernel/cbytegen.mli
index f33fd6cb..d0bfd46c 100644
--- a/kernel/cbytegen.mli
+++ b/kernel/cbytegen.mli
@@ -7,20 +7,21 @@ open Pre_env
val compile : env -> constr -> bytecodes * bytecodes * fv
- (* init, fun, fv *)
+ (** init, fun, fv *)
-val compile_constant_body :
- env -> constr_substituted option -> bool -> bool -> body_code
- (* opaque *) (* boxed *)
+val compile_constant_body : env -> constant_def -> body_code
+(** Shortcut of the previous function used during module strengthening *)
-(* spiwack: this function contains the information needed to perform
+val compile_alias : constant -> body_code
+
+(** spiwack: this function contains the information needed to perform
the static compilation of int31 (trying and obtaining
a 31-bit integer in processor representation at compile time) *)
val compile_structured_int31 : bool -> constr array ->
structured_constant
-(* this function contains the information needed to perform
+(** this function contains the information needed to perform
the dynamic compilation of int31 (trying and obtaining a
31-bit integer in processor representation at runtime when
it failed at compile time *)