Rename VM-related kernel/cfoo files to kernel/vmfoo

21 files changed, 41 insertions, 41 deletions

diff --git a/kernel/declarations.ml b/kernel/declarations.ml
index 7609c1a64d..9c32cd8e0e 100644
--- a/kernel/declarations.ml
+++ b/kernel/declarations.ml
@@ -107,7 +107,7 @@ type 'opaque constant_body = {
     const_body : (Constr.t Mod_subst.substituted, 'opaque) constant_def;
     const_type : types;
     const_relevance : Sorts.relevance;
-    const_body_code : Cemitcodes.to_patch_substituted option;
+    const_body_code : Vmemitcodes.to_patch_substituted option;
     const_universes : universes;
     const_inline_code : bool;
     const_typing_flags : typing_flags; (** The typing options which
diff --git a/kernel/declareops.ml b/kernel/declareops.ml
index 326bf0d6ad..b9f434f179 100644
--- a/kernel/declareops.ml
+++ b/kernel/declareops.ml
@@ -116,7 +116,7 @@ let subst_const_body sub cb =
         const_body = body';
         const_type = type';
         const_body_code =
-          Option.map (Cemitcodes.subst_to_patch_subst sub) cb.const_body_code;
+          Option.map (Vmemitcodes.subst_to_patch_subst sub) cb.const_body_code;
         const_universes = cb.const_universes;
         const_relevance = cb.const_relevance;
         const_inline_code = cb.const_inline_code;
diff --git a/kernel/dune b/kernel/dune
index 5f7502ef6b..ce6fdc03df 100644
--- a/kernel/dune
+++ b/kernel/dune
@@ -11,7 +11,7 @@
   (modules genOpcodeFiles))
 
 (rule
- (targets copcodes.ml)
+ (targets vmopcodes.ml)
  (action (with-stdout-to %{targets} (run ./genOpcodeFiles.exe copml))))
 
 (rule
diff --git a/kernel/genOpcodeFiles.ml b/kernel/genOpcodeFiles.ml
index 67a672c349..2d74cca44c 100644
--- a/kernel/genOpcodeFiles.ml
+++ b/kernel/genOpcodeFiles.ml
@@ -11,7 +11,7 @@
 (** List of opcodes.
 
     It is used to generate the [coq_instruct.h], [coq_jumptbl.h] and
-    [copcodes.ml] files.
+    [vmopcodes.ml] files.
 
     If adding an instruction, DON'T FORGET TO UPDATE coq_fix_code.c
     with the arity of the instruction and maybe coq_tcode_of_code.
@@ -196,7 +196,7 @@ let pp_coq_instruct_h fmt =
 let pp_coq_jumptbl_h fmt =
   pp_with_commas fmt (fun fmt -> Format.fprintf fmt "&&coq_lbl_%s")
 
-let pp_copcodes_ml fmt =
+let pp_vmopcodes_ml fmt =
   pp_header true fmt;
   Array.iteri (fun n s ->
       Format.fprintf fmt "let op%s = %d@.@." s n
@@ -210,7 +210,7 @@ let main () =
   match Sys.argv.(1) with
   | "enum" -> pp_coq_instruct_h Format.std_formatter
   | "jump" -> pp_coq_jumptbl_h Format.std_formatter
-  | "copml" -> pp_copcodes_ml Format.std_formatter
+  | "copml" -> pp_vmopcodes_ml Format.std_formatter
   | _ -> usage ()
   | exception Invalid_argument _ -> usage ()
 
diff --git a/kernel/kernel.mllib b/kernel/kernel.mllib
index 41388d9f17..d4d7150222 100644
--- a/kernel/kernel.mllib
+++ b/kernel/kernel.mllib
@@ -15,9 +15,9 @@ Term
 CPrimitives
 Mod_subst
 Vmvalues
-Cbytecodes
-Copcodes
-Cemitcodes
+Vmbytecodes
+Vmopcodes
+Vmemitcodes
 Opaqueproof
 Declarations
 Entries
@@ -30,12 +30,12 @@ Primred
 CClosure
 Relevanceops
 Reduction
-Clambda
+Vmlambda
 Nativelambda
-Cbytegen
+Vmbytegen
 Nativecode
 Nativelib
-Csymtable
+Vmsymtable
 Vm
 Vconv
 Nativeconv
diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml
index 44b010204b..5873d1f502 100644
--- a/kernel/mod_typing.ml
+++ b/kernel/mod_typing.ml
@@ -124,8 +124,8 @@ let rec check_with_def env struc (idl,(c,ctx)) mp equiv =
         { cb with
           const_body = def;
           const_universes = univs ;
-          const_body_code = Option.map Cemitcodes.from_val
-              (Cbytegen.compile_constant_body ~fail_on_error:false env' cb.const_universes def) }
+          const_body_code = Option.map Vmemitcodes.from_val
+              (Vmbytegen.compile_constant_body ~fail_on_error:false env' cb.const_universes def) }
       in
       before@(lab,SFBconst(cb'))::after, c', ctx'
     else
diff --git a/kernel/modops.ml b/kernel/modops.ml
index 77ef38dfd5..883ad79be5 100644
--- a/kernel/modops.ml
+++ b/kernel/modops.ml
@@ -328,7 +328,7 @@ let strengthen_const mp_from l cb resolver =
     let u = Univ.make_abstract_instance (Declareops.constant_polymorphic_context cb) in
       { cb with
         const_body = Def (Mod_subst.from_val (mkConstU (con,u)));
-        const_body_code = Some (Cemitcodes.from_val (Cbytegen.compile_alias con)) }
+        const_body_code = Some (Vmemitcodes.from_val (Vmbytegen.compile_alias con)) }
 
 let rec strengthen_mod mp_from mp_to mb =
   if mp_in_delta mb.mod_mp mb.mod_delta then mb
diff --git a/kernel/nativelambda.ml b/kernel/nativelambda.ml
index b00b96018f..99090f0147 100644
--- a/kernel/nativelambda.ml
+++ b/kernel/nativelambda.ml
@@ -395,8 +395,8 @@ let rec get_alias env (kn, u as p) =
     match tps with
     | None -> p
     | Some tps ->
-       match Cemitcodes.force tps with
-       | Cemitcodes.BCalias kn' -> get_alias env (kn', u)
+       match Vmemitcodes.force tps with
+       | Vmemitcodes.BCalias kn' -> get_alias env (kn', u)
        | _ -> p
 
 let prim env kn p args =
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index 48567aa564..24aa4ed771 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -283,8 +283,8 @@ let build_constant_declaration env result =
   let univs = result.cook_universes in
   let hyps = List.filter (fun d -> Id.Set.mem (NamedDecl.get_id d) hyps) (Environ.named_context env) in
   let tps =
-    let res = Cbytegen.compile_constant_body ~fail_on_error:false env univs def in
-    Option.map Cemitcodes.from_val res
+    let res = Vmbytegen.compile_constant_body ~fail_on_error:false env univs def in
+    Option.map Vmemitcodes.from_val res
   in
   { const_hyps = hyps;
     const_body = def;
@@ -343,8 +343,8 @@ let translate_recipe env _kn r =
   let open Cooking in
   let result = Cooking.cook_constant r in
   let univs = result.cook_universes in
-  let res = Cbytegen.compile_constant_body ~fail_on_error:false env univs result.cook_body in
-  let tps = Option.map Cemitcodes.from_val res in
+  let res = Vmbytegen.compile_constant_body ~fail_on_error:false env univs result.cook_body in
+  let tps = Option.map Vmemitcodes.from_val res in
   let hyps = Option.get result.cook_context in
   (* Trust the set of section hypotheses generated by Cooking *)
   let hyps = List.filter (fun d -> Id.Set.mem (NamedDecl.get_id d) hyps) (Environ.named_context env) in
diff --git a/kernel/vconv.ml b/kernel/vconv.ml
index f78f0d4d1e..cc2c2c0b4b 100644
--- a/kernel/vconv.ml
+++ b/kernel/vconv.ml
@@ -4,7 +4,7 @@ open Environ
 open Reduction
 open Vm
 open Vmvalues
-open Csymtable
+open Vmsymtable
 
 (* Test la structure des piles *)
 
diff --git a/kernel/vm.ml b/kernel/vm.ml
index d8c66bebd2..76954a83d8 100644
--- a/kernel/vm.ml
+++ b/kernel/vm.ml
@@ -44,7 +44,7 @@ external coq_interprete : tcode -> values -> atom array -> vm_global -> vm_env -
   "coq_interprete_byte" "coq_interprete_ml"
 
 let interprete code v env k =
-  coq_interprete code v (get_atom_rel ()) (Csymtable.get_global_data ()) env k
+  coq_interprete code v (get_atom_rel ()) (Vmsymtable.get_global_data ()) env k
 
 (* Functions over arguments *)
 
diff --git a/kernel/cbytecodes.ml b/kernel/vmbytecodes.ml
index 74405a0105..74405a0105 100644
--- a/kernel/cbytecodes.ml
+++ b/kernel/vmbytecodes.ml
diff --git a/kernel/cbytecodes.mli b/kernel/vmbytecodes.mli
index b703058fb7..b703058fb7 100644
--- a/kernel/cbytecodes.mli
+++ b/kernel/vmbytecodes.mli
diff --git a/kernel/cbytegen.ml b/kernel/vmbytegen.ml
index bacc308e1f..1274e3a867 100644
--- a/kernel/cbytegen.ml
+++ b/kernel/vmbytegen.ml
@@ -15,9 +15,9 @@
 open Util
 open Names
 open Vmvalues
-open Cbytecodes
-open Cemitcodes
-open Clambda
+open Vmbytecodes
+open Vmemitcodes
+open Vmlambda
 open Constr
 open Declarations
 open Environ
@@ -116,7 +116,7 @@ end
 
 module FvMap = Map.Make(Fv_elem)
 
-(*spiwack: both type have been moved from Cbytegen because I needed then
+(*spiwack: both type have been moved from Vmbytegen because I needed then
   for the retroknowledge *)
 type vm_env = {
     size : int;              (* longueur de la liste [n] *)
@@ -512,7 +512,7 @@ let rec get_alias env kn =
     match tps with
     | None -> kn
     | Some tps ->
-       (match Cemitcodes.force tps with
+       (match Vmemitcodes.force tps with
         | BCalias kn' -> get_alias env kn'
         | _ -> kn)
 
diff --git a/kernel/cbytegen.mli b/kernel/vmbytegen.mli
index d5ea2509ef..aef7ac3d6b 100644
--- a/kernel/cbytegen.mli
+++ b/kernel/vmbytegen.mli
@@ -8,8 +8,8 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-open Cbytecodes
-open Cemitcodes
+open Vmbytecodes
+open Vmemitcodes
 open Constr
 open Declarations
 open Environ
diff --git a/kernel/cemitcodes.ml b/kernel/vmemitcodes.ml
index ed475dca7e..2dfc9a2941 100644
--- a/kernel/cemitcodes.ml
+++ b/kernel/vmemitcodes.ml
@@ -14,8 +14,8 @@
 
 open Names
 open Vmvalues
-open Cbytecodes
-open Copcodes
+open Vmbytecodes
+open Vmopcodes
 open Mod_subst
 open CPrimitives
 
@@ -350,7 +350,7 @@ let emit_instr env = function
   | Ksetfield n ->
       if n <= 1 then out env (opSETFIELD0+n)
       else (out env opSETFIELD;out_int env n)
-  | Ksequence _ -> invalid_arg "Cemitcodes.emit_instr"
+  | Ksequence _ -> invalid_arg "Vmemitcodes.emit_instr"
   | Kproj p -> out env opPROJ; out_int env (Projection.Repr.arg p); slot_for_proj_name env p
   | Kensurestackcapacity size -> out env opENSURESTACKCAPACITY; out_int env size
   | Kbranch lbl -> out env opBRANCH; out_label env lbl
diff --git a/kernel/cemitcodes.mli b/kernel/vmemitcodes.mli
index c4262f3380..5c0e103143 100644
--- a/kernel/cemitcodes.mli
+++ b/kernel/vmemitcodes.mli
@@ -9,7 +9,7 @@
 (************************************************************************)
 open Names
 open Vmvalues
-open Cbytecodes
+open Vmbytecodes
 
 type reloc_info =
   | Reloc_annot of annot_switch
diff --git a/kernel/clambda.ml b/kernel/vmlambda.ml
index 6690a379ce..332a331a7a 100644
--- a/kernel/clambda.ml
+++ b/kernel/vmlambda.ml
@@ -559,8 +559,8 @@ let rec get_alias env kn =
   match tps with
   | None -> kn
   | Some tps ->
-    (match Cemitcodes.force tps with
-     | Cemitcodes.BCalias kn' -> get_alias env kn'
+    (match Vmemitcodes.force tps with
+     | Vmemitcodes.BCalias kn' -> get_alias env kn'
      | _ -> kn)
 
 (* Compilation of primitive *)
@@ -681,7 +681,7 @@ open Renv
 
 let rec lambda_of_constr env c =
   match Constr.kind c with
-  | Meta _ -> raise (Invalid_argument "Cbytegen.lambda_of_constr: Meta")
+  | Meta _ -> raise (Invalid_argument "Vmbytegen.lambda_of_constr: Meta")
   | Evar (evk, args) ->
     let args = Array.map_of_list (fun c -> lambda_of_constr env c) args in
     Levar (evk, args)
diff --git a/kernel/clambda.mli b/kernel/vmlambda.mli
index bd11c2667f..bd11c2667f 100644
--- a/kernel/clambda.mli
+++ b/kernel/vmlambda.mli
diff --git a/kernel/csymtable.ml b/kernel/vmsymtable.ml
index 185fb9f5a4..85f7369654 100644
--- a/kernel/csymtable.ml
+++ b/kernel/vmsymtable.ml
@@ -17,11 +17,11 @@
 open Util
 open Names
 open Vmvalues
-open Cemitcodes
-open Cbytecodes
+open Vmemitcodes
+open Vmbytecodes
 open Declarations
 open Environ
-open Cbytegen
+open Vmbytegen
 
 module NamedDecl = Context.Named.Declaration
 module RelDecl = Context.Rel.Declaration
@@ -155,7 +155,7 @@ let rec slot_for_getglobal env kn =
       match cb.const_body_code with
       | None -> set_global (val_of_constant kn)
       | Some code ->
-         match Cemitcodes.force code with
+         match Vmemitcodes.force code with
          | BCdefined(code,pl,fv) ->
            let v = eval_to_patch env (code,pl,fv) in
            set_global v
diff --git a/kernel/csymtable.mli b/kernel/vmsymtable.mli
index e480bfcec1..e480bfcec1 100644
--- a/kernel/csymtable.mli
+++ b/kernel/vmsymtable.mli