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