diff options
| author | aspiwack | 2013-11-02 15:40:07 +0000 |
|---|---|---|
| committer | aspiwack | 2013-11-02 15:40:07 +0000 |
| commit | a774fb3002f72a24b62415478cb8dd0cc7e5d708 (patch) | |
| tree | 8735f84013f8b08ed444eac7fd7c870aa9bbd97e /tactics | |
| parent | d4023190339a89484ab78074051e2e3029133708 (diff) | |
Made multiple-goal tactic work after all: .
Internalization was done relative to a goal. It doesn't make sense in the
case of all:. When we make a tactic with all: the environment for
internalization is taken to be the global environment.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17016 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/tacinterp.ml | 17 | ||||
| -rw-r--r-- | tactics/tacinterp.mli | 2 |
2 files changed, 13 insertions, 6 deletions
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index c430bcf828..cb4bc01a35 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -2363,10 +2363,9 @@ let eval_ltac_constr t = (intern_tactic_or_tacarg (make_empty_glob_sign ()) t ) (* Used to hide interpretation for pretty-print, now just launch tactics *) -let hide_interp t ot = - Proofview.Goal.enter begin fun gl -> - let env = Proofview.Goal.env gl in - let sigma = Proofview.Goal.sigma gl in +(* [global] means that [t] should be internalized outside of goals. *) +let hide_interp global t ot = + let hide_interp env sigma = let ist = { ltacvars = Id.Set.empty; ltacrecvars = Id.Map.empty; gsigma = sigma; genv = env } in let te = intern_pure_tactic ist t in @@ -2374,7 +2373,15 @@ let hide_interp t ot = match ot with | None -> t | Some t' -> Tacticals.New.tclTHEN t t' - end + in + if global then + Proofview.tclENV >= fun env -> + Proofview.tclEVARMAP >= fun sigma -> + hide_interp env sigma + else + Proofview.Goal.enter begin fun gl -> + hide_interp (Proofview.Goal.env gl) (Proofview.Goal.sigma gl) + end (***************************************************************************) (** Register standard arguments *) diff --git a/tactics/tacinterp.mli b/tactics/tacinterp.mli index 9eb4b3650d..ce6639d4ba 100644 --- a/tactics/tacinterp.mli +++ b/tactics/tacinterp.mli @@ -110,7 +110,7 @@ val eval_ltac_constr : raw_tactic_expr -> constr Proofview.glist Proofview.tacti (** Hides interpretation for pretty-print *) -val hide_interp : raw_tactic_expr -> unit Proofview.tactic option -> unit Proofview.tactic +val hide_interp : bool -> raw_tactic_expr -> unit Proofview.tactic option -> unit Proofview.tactic (** Declare the xml printer *) val declare_xml_printer : |