diff options
| author | Jason Gross | 2019-03-31 15:00:00 -0400 |
|---|---|---|
| committer | Jason Gross | 2019-04-01 11:08:54 -0400 |
| commit | 67e93e9ff5e5b1723ff62da8a82782e5030b5721 (patch) | |
| tree | 6ee0ab4995f5ec9a400b8f0cb36ce51feee62f1d /kernel/nativelambda.mli | |
| parent | b0f8e09c3212fa96934817e7ca99465cd634f57c (diff) | |
[numeral] Add a case for IndRef in constr_of_glob
Fixes #9840
Diffstat (limited to 'kernel/nativelambda.mli')
0 files changed, 0 insertions, 0 deletions