diff options
author | 2017-09-08 14:58:28 +0200 | |
---|---|---|
committer | 2017-09-08 18:42:37 +0200 | |
commit | b71e68fb78ccde52f1aaa63ef26f0135b92e9be5 (patch) | |
tree | fd07ca12f3aa602a082cc960a82f031ea72fa7c3 /pretyping/typing.ml | |
parent | b1fbec7e3945fe2965f4ba9f80c8c31b821dbce1 (diff) |
Parse directly to Sorts.family when appropriate.
When we used to parse to a glob_sort but always give an empty list in
the GType case we can now parse directly to Sorts.family.
Diffstat (limited to 'pretyping/typing.ml')
0 files changed, 0 insertions, 0 deletions