diff options
author | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-03-02 15:50:32 +0100 |
---|---|---|
committer | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-04-17 16:29:07 +0200 |
commit | dbc820f0df53218e730eba34b44a3b1901f13b9e (patch) | |
tree | 11720b5f35bbc51202eec80e27eca14e32f8064c /tactics | |
parent | 3e7863e9369d38537685576a8642dbe0c062d0c5 (diff) |
Deprecate mixing univ minimization and evm normalization functions.
Normalization sounds like it should be semantically noop.
Diffstat (limited to 'tactics')
-rw-r--r-- | tactics/elimschemes.ml | 4 | ||||
-rw-r--r-- | tactics/tactics.ml | 4 |
2 files changed, 4 insertions, 4 deletions
diff --git a/tactics/elimschemes.ml b/tactics/elimschemes.ml index 6bd4866c6..70f73df5c 100644 --- a/tactics/elimschemes.ml +++ b/tactics/elimschemes.ml @@ -46,8 +46,8 @@ let optimize_non_type_induction_scheme kind dep sort _ ind = mib.mind_nparams in let sigma, sort = Evd.fresh_sort_in_family env sigma sort in let sigma, t', c' = weaken_sort_scheme env sigma false sort npars c t in - let sigma, nf = Evarutil.nf_evars_and_universes sigma in - (nf c', Evd.evar_universe_context sigma), eff + let sigma = Evd.minimize_universes sigma in + (Evarutil.nf_evars_universes sigma c', Evd.evar_universe_context sigma), eff else let sigma, pind = Evd.fresh_inductive_instance env sigma ind in let sigma, c = build_induction_scheme env sigma pind dep sort in diff --git a/tactics/tactics.ml b/tactics/tactics.ml index aae4bc088..482571ea8 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -4929,9 +4929,9 @@ let cache_term_by_tactic_then ~opaque ?(goal_type=None) id gk tac tacK = let evd, ctx, concl = (* FIXME: should be done only if the tactic succeeds *) - let evd, nf = nf_evars_and_universes !evdref in + let evd = Evd.minimize_universes !evdref in let ctx = Evd.universe_context_set evd in - evd, ctx, nf concl + evd, ctx, Evarutil.nf_evars_universes evd concl in let concl = EConstr.of_constr concl in let solve_tac = tclCOMPLETE (tclTHEN (tclDO (List.length sign) intro) tac) in |