From 5d926b0279f70250db1ee54edcdb4e855ac96f0f Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Fri, 2 Mar 2018 14:58:00 +0100 Subject: Deprecate UState aliases in Evd. --- tactics/ind_tables.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'tactics/ind_tables.ml') diff --git a/tactics/ind_tables.ml b/tactics/ind_tables.ml index b960a845c..71e2d5820 100644 --- a/tactics/ind_tables.ml +++ b/tactics/ind_tables.ml @@ -122,8 +122,8 @@ let compute_name internal id = let define internal id c p univs = let fd = declare_constant ~internal in let id = compute_name internal id in - let ctx = Evd.normalize_evar_universe_context univs in - let c = Universes.subst_opt_univs_constr (Evd.evar_universe_context_subst ctx) c in + let ctx = UState.normalize univs in + let c = Universes.subst_opt_univs_constr (UState.subst ctx) c in let univs = if p then Polymorphic_const_entry (UState.context ctx) else Monomorphic_const_entry (UState.context_set ctx) -- cgit v1.2.3