diff options
Diffstat (limited to 'tactics/auto.ml')
| -rw-r--r-- | tactics/auto.ml | 9 |
1 files changed, 5 insertions, 4 deletions
diff --git a/tactics/auto.ml b/tactics/auto.ml index 617c491c3..9ca6162a2 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -117,10 +117,11 @@ let exact poly (c,clenv) = let ctx = Evd.evar_universe_context clenv.evd in ctx, c in - Proofview.Goal.enter begin fun gl -> - let sigma = Evd.merge_universe_context (Proofview.Goal.sigma gl) ctx in - Tacticals.New.tclTHEN (Proofview.Unsafe.tclEVARS sigma) (exact_check c') - end + Proofview.Goal.s_enter { enter = begin fun gl sigma -> + let sigma = Sigma.to_evar_map sigma in + let sigma = Evd.merge_universe_context sigma ctx in + Sigma.Unsafe.of_pair (exact_check c', sigma) + end } (* Util *) |