diff options
| author | Gaëtan Gilbert | 2018-10-10 14:20:51 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2018-10-16 15:52:53 +0200 |
| commit | 44ecd58e9ab5fb0f2c45e9eec76440f84995825c (patch) | |
| tree | 5ce39ab09db09194d5a28ee48cd4a7ee7643b4fc /kernel/type_errors.mli | |
| parent | e99b4c66cf38bb5b6ccb76b69ebd7e7a44ed295d (diff) | |
{Univops -> Vars}.universes_of_constr
It's basically an occur check so it makes sense to put it in vars
Diffstat (limited to 'kernel/type_errors.mli')
0 files changed, 0 insertions, 0 deletions