aboutsummaryrefslogtreecommitdiff
path: root/interp/stdarg.ml
diff options
context:
space:
mode:
authorcoqbot-app[bot]2020-11-20 09:32:34 +0000
committerGitHub2020-11-20 09:32:34 +0000
commita8a0285c153cab810dedba6bae5a2a6a6d2c4333 (patch)
treec328b81d028179b5a9c0cc68ec385d232e09daba /interp/stdarg.ml
parent122aef582e69f692e6720097a3fac7e0d4d41bcd (diff)
parentf6a8c2542a5ce85a91caf9b1745c980c2164707a (diff)
Merge PR #13360: Fix incorrect name refreshing when interning a generalized binder
Reviewed-by: herbelin
Diffstat (limited to 'interp/stdarg.ml')
0 files changed, 0 insertions, 0 deletions