aboutsummaryrefslogtreecommitdiff
path: root/kernel/genOpcodeFiles.ml
diff options
context:
space:
mode:
authorGuillaume Melquiond2021-02-17 12:12:29 +0100
committerGuillaume Melquiond2021-02-19 11:17:26 +0100
commitab94a2a5dbe142d972d65a33d977e8e9f8d52f01 (patch)
tree45b6fb6ea9fc2a13c1b02a0bbb2800ad3a2f4458 /kernel/genOpcodeFiles.ml
parentc7bbe4729dc53ddf3a02a7ae3816ec3c146d452e (diff)
Make the generated file the official source of arity.
Diffstat (limited to 'kernel/genOpcodeFiles.ml')
-rw-r--r--kernel/genOpcodeFiles.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/genOpcodeFiles.ml b/kernel/genOpcodeFiles.ml
index 25da7c2685..bda65956be 100644
--- a/kernel/genOpcodeFiles.ml
+++ b/kernel/genOpcodeFiles.ml
@@ -178,7 +178,7 @@ let pp_coq_jumptbl_h fmt =
let pp_coq_arity_h fmt =
pp_header false fmt;
- Format.fprintf fmt "static signed char arity2[] = {@.";
+ Format.fprintf fmt "static signed char arity[] = {@.";
Array.iter (fun (_, arity) ->
Format.fprintf fmt " %d,@." arity
) opcodes;