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/tactics.ml | |
| parent | 3e7863e9369d38537685576a8642dbe0c062d0c5 (diff) | |
Deprecate mixing univ minimization and evm normalization functions.
Normalization sounds like it should be semantically noop.
Diffstat (limited to 'tactics/tactics.ml')
| -rw-r--r-- | tactics/tactics.ml | 4 |
1 files changed, 2 insertions, 2 deletions
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 |