diff options
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 : |