diff options
| author | coqbot-app[bot] | 2020-11-20 09:21:27 +0000 |
|---|---|---|
| committer | GitHub | 2020-11-20 09:21:27 +0000 |
| commit | 122aef582e69f692e6720097a3fac7e0d4d41bcd (patch) | |
| tree | 062a2e1a02e687d5f5fe68b6dd949ee2b4c9dbae /interp | |
| parent | 57c85b0d54e54ca33238399cab3285ef34d4edd2 (diff) | |
| parent | 00003b625ed3d5f3f2d79cf38ca6ad08e634432e (diff) | |
Merge PR #13403: Use only nats for occs_nums rather than ints
Reviewed-by: Zimmi48
Reviewed-by: herbelin
Diffstat (limited to 'interp')
0 files changed, 0 insertions, 0 deletions