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

28 files changed, 52 insertions, 51 deletions

diff --git a/.github/CODEOWNERS b/.github/CODEOWNERS
index 8dbdf43e52..5130fd02b6 100644
--- a/.github/CODEOWNERS
+++ b/.github/CODEOWNERS
@@ -103,6 +103,7 @@
 /kernel/native*   @coq/vm-native-maintainers
 /kernel/vm*       @coq/vm-native-maintainers
 /kernel/vconv.*   @coq/vm-native-maintainers
+/kernel/genOpcodefiles.* @coq/vm-native-maintainers
 
 /kernel/sorts.*   @coq/universes-maintainers
 /kernel/uGraph.*  @coq/universes-maintainers
diff --git a/Makefile.build b/Makefile.build
index 7806dce79c..4fb4b12be2 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -367,7 +367,7 @@ kernel/byterun/coq_jumptbl.h: kernel/genOpcodeFiles.exe
 	$(SHOW)'WRITE $@'
 	$(HIDE)$< jump > $@
 
-kernel/copcodes.ml: kernel/genOpcodeFiles.exe
+kernel/vmopcodes.ml: kernel/genOpcodeFiles.exe
 	$(SHOW)'WRITE $@'
 	$(HIDE)$< copml > $@
 
diff --git a/Makefile.make b/Makefile.make
index 7191738612..51d6d1c3c1 100644
--- a/Makefile.make
+++ b/Makefile.make
@@ -107,7 +107,7 @@ GRAMMLIFILES := $(addsuffix .mli, $(GRAMFILES))
 GENGRAMMLFILES := $(GRAMMLFILES) gramlib/.pack/gramlib.ml # why is gramlib.ml not in GRAMMLFILES?
 
 GENMLGFILES:= $(MLGFILES:.mlg=.ml)
-GENMLFILES:=$(LEXFILES:.mll=.ml) $(YACCFILES:.mly=.ml) $(GENMLGFILES) $(GENGRAMMLFILES) ide/coqide/coqide_os_specific.ml kernel/copcodes.ml kernel/uint63.ml
+GENMLFILES:=$(LEXFILES:.mll=.ml) $(YACCFILES:.mly=.ml) $(GENMLGFILES) $(GENGRAMMLFILES) ide/coqide/coqide_os_specific.ml kernel/vmopcodes.ml kernel/uint63.ml
 GENMLIFILES:=$(GRAMMLIFILES)
 GENHFILES:=kernel/byterun/coq_instruct.h kernel/byterun/coq_jumptbl.h
 GENFILES:=$(GENMLFILES) $(GENMLIFILES) $(GENHFILES) kernel/genOpcodeFiles.exe
diff --git a/dev/vm_printers.ml b/dev/vm_printers.ml
index ac4972ed0d..1eacfa0fd6 100644
--- a/dev/vm_printers.ml
+++ b/dev/vm_printers.ml
@@ -1,7 +1,7 @@
 open Format
 open Term
 open Names
-open Cemitcodes
+open Vmemitcodes
 open Vmvalues
 
 let ppripos (ri,pos) =
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
diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml
index e5fa9bada1..900ba0edb9 100644
--- a/pretyping/vnorm.ml
+++ b/pretyping/vnorm.ml
@@ -415,7 +415,7 @@ let cbv_vm env sigma c t  =
   (* This evar-normalizes terms beforehand *)
   let c = EConstr.to_constr ~abort_on_undefined_evars:false sigma c in
   let t = EConstr.to_constr ~abort_on_undefined_evars:false sigma t in
-  let v = Csymtable.val_of_constr env c in
+  let v = Vmsymtable.val_of_constr env c in
   EConstr.of_constr (nf_val env sigma v t)
 
 let vm_infer_conv ?(pb=Reduction.CUMUL) env sigma t1 t2 =
diff --git a/tactics/redexpr.ml b/tactics/redexpr.ml
index c463c06cd5..a8747e0a7c 100644
--- a/tactics/redexpr.ml
+++ b/tactics/redexpr.ml
@@ -60,7 +60,7 @@ let set_strategy_one ref l  =
   Global.set_strategy k l;
   match k,l with
       ConstKey sp, Conv_oracle.Opaque ->
-        Csymtable.set_opaque_const sp
+        Vmsymtable.set_opaque_const sp
     | ConstKey sp, _ ->
         let cb = Global.lookup_constant sp in
         (match cb.const_body with
@@ -69,7 +69,7 @@ let set_strategy_one ref l  =
               (str "Cannot make" ++ spc () ++
                  Nametab.pr_global_env Id.Set.empty (GlobRef.ConstRef sp) ++
                  spc () ++ str "transparent because it was declared opaque.");
-          | _ -> Csymtable.set_transparent_const sp)
+          | _ -> Vmsymtable.set_transparent_const sp)
     | _ -> ()
 
 let cache_strategy (_,str) =
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index d540e7f93d..4262563686 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -1511,15 +1511,15 @@ let () =
   declare_bool_option
     { optdepr  = false;
       optkey   = ["Dump";"Bytecode"];
-      optread  = (fun () -> !Cbytegen.dump_bytecode);
-      optwrite = (:=) Cbytegen.dump_bytecode }
+      optread  = (fun () -> !Vmbytegen.dump_bytecode);
+      optwrite = (:=) Vmbytegen.dump_bytecode }
 
 let () =
   declare_bool_option
     { optdepr  = false;
       optkey   = ["Dump";"Lambda"];
-      optread  = (fun () -> !Clambda.dump_lambda);
-      optwrite = (:=) Clambda.dump_lambda }
+      optread  = (fun () -> !Vmlambda.dump_lambda);
+      optwrite = (:=) Vmlambda.dump_lambda }
 
 let () =
   declare_bool_option