Merge PR #12849: Rename VM-related kernel/cfoo files to kernel/vmfoo

Reviewed-by: gares
Reviewed-by: ppedrot
Reviewed-by: silene

1 files changed, 31 insertions, 0 deletions

diff --git a/kernel/vmbytegen.mli b/kernel/vmbytegen.mli
new file mode 100644
index 0000000000..aef7ac3d6b
--- /dev/null
+++ b/kernel/vmbytegen.mli
@@ -0,0 +1,31 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *         Copyright INRIA, CNRS and contributors             *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+open Vmbytecodes
+open Vmemitcodes
+open Constr
+open Declarations
+open Environ
+
+(** Should only be used for monomorphic terms *)
+val compile : fail_on_error:bool ->
+              ?universes:int -> env -> constr -> (bytecodes * bytecodes * fv) option
+(** init, fun, fv *)
+
+val compile_constant_body : fail_on_error:bool ->
+  env -> universes -> (Constr.t Mod_subst.substituted, 'opaque) constant_def ->
+  body_code option
+
+(** Shortcut of the previous function used during module strengthening *)
+
+val compile_alias : Names.Constant.t -> body_code
+
+(** Dump the bytecode after compilation (for debugging purposes) *)
+val dump_bytecode : bool ref