From 6aa0aa37e19457a8c0c3ad36f7bbead058442344 Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Wed, 10 Oct 2018 14:41:31 +0200 Subject: {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 --- plugins/setoid_ring/newring.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'plugins') 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), -- cgit v1.2.3