diff options
| -rw-r--r-- | tactics/tacinterp.ml | 17 | ||||
| -rw-r--r-- | tactics/tacinterp.mli | 2 | ||||
| -rw-r--r-- | toplevel/vernacentries.ml | 5 |
3 files changed, 17 insertions, 7 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 : diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 7655d3032d..48961fa9df 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -777,7 +777,10 @@ let vernac_solve n tcom b = error "Unknown command of the non proof-editing mode."; let status = Proof_global.with_current_proof (fun etac p -> let with_end_tac = if b then Some etac else None in - let (p,status) = solve n (Tacinterp.hide_interp tcom None) ?with_end_tac p in + let global = match n with SelectAll -> true | _ -> false in + let (p,status) = + solve n (Tacinterp.hide_interp global tcom None) ?with_end_tac p + in (* in case a strict subtree was completed, go back to the top of the prooftree *) let p = Proof.maximal_unfocus command_focus p in |