diff options
| author | Pierre-Marie Pédrot | 2019-02-05 17:35:01 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-02-11 15:48:43 +0100 |
| commit | 81c6a0873d90bfa3909c2046054c21096f80eb07 (patch) | |
| tree | 7ede6b00bb6f9eb1f73a24bfc212052830365946 /kernel/type_errors.ml | |
| parent | fba77d134e27c086a982e61de5741038bf92bb8a (diff) | |
Specialize the intermediate types of the Grammar functor.
Now that we depend on a module argument, we do not have to quantify
over the arguments anymore.
Diffstat (limited to 'kernel/type_errors.ml')
0 files changed, 0 insertions, 0 deletions