diff options
| author | Pierre-Marie Pédrot | 2020-08-27 16:50:45 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-08-27 16:50:45 +0200 |
| commit | 1abf7c94f97948f8171c2fe1fec99cd890e8d1f6 (patch) | |
| tree | 3c60f0cd4a38608dacceca0b012de120bdc46a79 /kernel/genOpcodeFiles.ml | |
| parent | f140359a6df94d1caa2ccea3da2d48e01eacc44b (diff) | |
| parent | 4ee0cedff7726a56ebd53125995a7ae131660b4a (diff) | |
Merge PR #12849: Rename VM-related kernel/cfoo files to kernel/vmfoo
Reviewed-by: gares
Reviewed-by: ppedrot
Reviewed-by: silene
Diffstat (limited to 'kernel/genOpcodeFiles.ml')
| -rw-r--r-- | kernel/genOpcodeFiles.ml | 6 |
1 files changed, 3 insertions, 3 deletions
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 () |