diff options
| author | Gaëtan Gilbert | 2020-02-12 13:54:14 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-02-13 15:12:01 +0100 |
| commit | 3af570b60e6912d2eb906ce86a3df3b8ecca675c (patch) | |
| tree | 17005ee530a8447dc8d58b5e58ec23edebd5711e /kernel/subtyping.ml | |
| parent | e76b9da873d2e690e9dd24ed36ecec505676651e (diff) | |
Don't duplicate the inductive keyword for each block elt when parsing
Diffstat (limited to 'kernel/subtyping.ml')
0 files changed, 0 insertions, 0 deletions