aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/cbytegen.mli
diff options
context:
space:
mode:
Diffstat (limited to 'kernel/cbytegen.mli')
-rw-r--r--kernel/cbytegen.mli4
1 files changed, 2 insertions, 2 deletions
diff --git a/kernel/cbytegen.mli b/kernel/cbytegen.mli
index bf9c0be26..403c1c7b5 100644
--- a/kernel/cbytegen.mli
+++ b/kernel/cbytegen.mli
@@ -10,8 +10,8 @@ val compile : env -> constr -> bytecodes * bytecodes * fv
(** init, fun, fv *)
val compile_constant_body :
- env -> constr_substituted option -> bool -> bool -> body_code
- (** opaque *) (* boxed *)
+ env -> constr_substituted option -> bool -> body_code
+ (** opaque *)
(** spiwack: this function contains the information needed to perform