aboutsummaryrefslogtreecommitdiff
path: root/kernel/modops.mli
diff options
context:
space:
mode:
authorGuillaume Melquiond2021-02-17 12:09:00 +0100
committerGuillaume Melquiond2021-02-19 11:17:26 +0100
commitc7bbe4729dc53ddf3a02a7ae3816ec3c146d452e (patch)
tree18f2e1a463ae9c4106fbfe4703c2098ff740cf20 /kernel/modops.mli
parentbbb9876da3093658c9eca206a585b045ed258220 (diff)
Add a file coq_arity.h generated by genOpcodeFiles.ml.
This avoids forgetting to add opcodes to coq_fix_code.c, and thus prevents arities being mistakenly set to zero.
Diffstat (limited to 'kernel/modops.mli')
0 files changed, 0 insertions, 0 deletions