1 files changed, 17 insertions, 0 deletions
diff --git a/kernel/cbytegen.mli b/kernel/cbytegen.mli
new file mode 100644
index 00000000..f761e4f6
--- /dev/null
+++ b/kernel/cbytegen.mli
@@ -0,0 +1,17 @@
+open Names
+open Cbytecodes
+open Cemitcodes 
+open Term
+open Declarations
+open Pre_env
+
+
+
+val compile : env -> constr -> bytecodes * bytecodes * fv
+                              (* init, fun, fv *)
+
+val compile_constant_body : 
+    env -> constr_substituted option -> bool -> bool -> body_code
+                                 (* opaque *) (* boxed *)
+
+