diff options
| author | Maxime Dénès | 2018-01-08 12:46:22 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2018-01-08 12:46:22 +0100 |
| commit | 47f47713e551f8de18cf2d847f47c1f55b016c8b (patch) | |
| tree | fba8437d2bab7f202181c83a935ff24e865dcc69 /tactics | |
| parent | c34744837dae427ac6cb12f5ada198862d8e1e4f (diff) | |
| parent | 4131f060ac42f121685817fcc9546c3899c09ab7 (diff) | |
Merge PR #6425: Cleanup universes in the kernel
Diffstat (limited to 'tactics')
| -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 e1bf32f3ce..bc2fea2bd5 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) |