aboutsummaryrefslogtreecommitdiff
path: root/interp/stdarg.mli
diff options
context:
space:
mode:
authorcoqbot-app[bot]2020-11-20 09:21:27 +0000
committerGitHub2020-11-20 09:21:27 +0000
commit122aef582e69f692e6720097a3fac7e0d4d41bcd (patch)
tree062a2e1a02e687d5f5fe68b6dd949ee2b4c9dbae /interp/stdarg.mli
parent57c85b0d54e54ca33238399cab3285ef34d4edd2 (diff)
parent00003b625ed3d5f3f2d79cf38ca6ad08e634432e (diff)
Merge PR #13403: Use only nats for occs_nums rather than ints
Reviewed-by: Zimmi48 Reviewed-by: herbelin
Diffstat (limited to 'interp/stdarg.mli')
0 files changed, 0 insertions, 0 deletions