diff options
| author | Matthieu Sozeau | 2014-06-20 12:16:20 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2014-06-20 12:16:20 +0200 |
| commit | 8b90dc406730123640f186c8b39f6329a3f434a4 (patch) | |
| tree | 41d1a2787829d40d2acdce394be8c5df2408d07b /kernel/type_errors.ml | |
| parent | dbe87dc85d7bd1c7d597a7a6ee00ffc1b70948ad (diff) | |
Add an e_type_of to avoid losing universe constraints.
Diffstat (limited to 'kernel/type_errors.ml')
0 files changed, 0 insertions, 0 deletions