diff options
Diffstat (limited to 'tactics/evar_tactics.ml')
| -rw-r--r-- | tactics/evar_tactics.ml | 12 |
1 files changed, 7 insertions, 5 deletions
diff --git a/tactics/evar_tactics.ml b/tactics/evar_tactics.ml index 0555564bd..20f72b3d5 100644 --- a/tactics/evar_tactics.ml +++ b/tactics/evar_tactics.ml @@ -53,8 +53,10 @@ let instantiate n (ist,rawc) ido gl = open Proofview.Notations let let_evar name typ = let src = (Loc.ghost,Evar_kinds.GoalEvar) in - Proofview.tclEVARMAP >= fun sigma -> - Proofview.Goal.env >>= fun env -> - let sigma',evar = Evarutil.new_evar sigma env ~src typ in - Tacticals.New.tclTHEN (Proofview.V82.tactic (Refiner.tclEVARS sigma')) - (Tactics.letin_tac None name evar None Locusops.nowhere) + Proofview.Goal.enter begin fun gl -> + let sigma = Proofview.Goal.sigma gl in + let env = Proofview.Goal.env gl in + let sigma',evar = Evarutil.new_evar sigma env ~src typ in + Tacticals.New.tclTHEN (Proofview.V82.tactic (Refiner.tclEVARS sigma')) + (Tactics.letin_tac None name evar None Locusops.nowhere) + end |