aboutsummaryrefslogtreecommitdiff
path: root/engine/uState.ml
diff options
context:
space:
mode:
authorGaëtan Gilbert2018-10-10 14:20:51 +0200
committerGaëtan Gilbert2018-10-16 15:52:53 +0200
commit44ecd58e9ab5fb0f2c45e9eec76440f84995825c (patch)
tree5ce39ab09db09194d5a28ee48cd4a7ee7643b4fc /engine/uState.ml
parente99b4c66cf38bb5b6ccb76b69ebd7e7a44ed295d (diff)
{Univops -> Vars}.universes_of_constr
It's basically an occur check so it makes sense to put it in vars
Diffstat (limited to 'engine/uState.ml')
0 files changed, 0 insertions, 0 deletions