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

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