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 /plugins | |
| 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 'plugins')
| -rw-r--r-- | plugins/setoid_ring/newring.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml index cf959bd11f..9585826109 100644 --- a/plugins/setoid_ring/newring.ml +++ b/plugins/setoid_ring/newring.ml @@ -152,7 +152,7 @@ let ic_unsafe c = (*FIXME remove *) let decl_constant na univs c = let open Constr in let vars = CVars.universes_of_constr c in - let univs = Univops.restrict_universe_context univs vars in + let univs = UState.restrict_universe_context univs vars in let univs = Monomorphic_const_entry univs in mkConst(declare_constant (Id.of_string na) (DefinitionEntry (definition_entry ~opaque:true ~univs c), |