diff options
Diffstat (limited to 'tactics/ind_tables.ml')
| -rw-r--r-- | tactics/ind_tables.ml | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/tactics/ind_tables.ml b/tactics/ind_tables.ml index e1bf32f3c..bc2fea2bd 100644 --- a/tactics/ind_tables.ml +++ b/tactics/ind_tables.ml @@ -121,8 +121,7 @@ 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 = Vars.subst_univs_fn_constr - (Universes.make_opt_subst (Evd.evar_universe_context_subst ctx)) c in + let c = Universes.subst_opt_univs_constr (Evd.evar_universe_context_subst ctx) c in let univs = if p then Polymorphic_const_entry (UState.context ctx) else Monomorphic_const_entry (UState.context_set ctx) |