diff options
| author | aspiwack | 2013-11-02 15:38:20 +0000 |
|---|---|---|
| committer | aspiwack | 2013-11-02 15:38:20 +0000 |
| commit | ea879916e09cd19287c831152d7ae2a84c61f4b0 (patch) | |
| tree | ba48057f7a5aa3fe160ba26313c5a74ec7a96162 /tactics/evar_tactics.ml | |
| parent | 07df7994675427b353004da666c23ae79444b0e5 (diff) | |
More Proofview.Goal.enter.
Proofview.Goal.enter is meant to eventually replace the Goal.sensitive monad.
This commit changes the type of Proofview.Goal.enter from taking a four argument function (environment, evar_map, hyps, concl) from a one argument function of abstract type Proofview.Goal.t. It will be both more extensible and more akin to old-style tactics.
This commit also changes the type of Proofview.Goal.{concl,hyps,env} from monadic operations to projection from a Proofview.Goal.t.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17000 85f007b7-540e-0410-9357-904b9bb8a0f7
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 0555564bd1..20f72b3d56 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 |