diff options
| author | Gaëtan Gilbert | 2018-10-10 14:41:31 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2018-10-16 15:52:53 +0200 |
| commit | 6aa0aa37e19457a8c0c3ad36f7bbead058442344 (patch) | |
| tree | 4a5e027fb684c4c3cc4f0627af24ba659a56e0b7 /engine/engine.mllib | |
| parent | 44ecd58e9ab5fb0f2c45e9eec76440f84995825c (diff) | |
{Univops->UState}.restrict_universe_context
Thus the adhoc univops can be removed at the end of the deprecation period.
Should we keep exposing restrict_universe_context or make people go
through restrict?
restrict_universe_context is used directly only by newring, where it's
a choice between
let univs = UState.restrict_universe_context univs vars in
and
let univs = UState.(context_set (restrict (of_context_set univs) vars)) in
Diffstat (limited to 'engine/engine.mllib')
| -rw-r--r-- | engine/engine.mllib | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/engine/engine.mllib b/engine/engine.mllib index 37e83b6238..bb43808542 100644 --- a/engine/engine.mllib +++ b/engine/engine.mllib @@ -4,8 +4,8 @@ UnivSubst UnivProblem UnivMinim Universes -Univops UState +Univops Nameops Evar_kinds Evd |