Removing the VernacSolve entry of the vernacular AST.

This is an important step into making Ltac a plugin. It also allows to
see what the important entry points in the Coq codebase for a tactic
language are.

19 files changed, 157 insertions, 137 deletions

diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli
index 5501ca7c7f..36b855ec3b 100644
--- a/intf/vernacexpr.mli
+++ b/intf/vernacexpr.mli
@@ -31,7 +31,6 @@ type goal_selector =
   | SelectNth of int
   | SelectId of Id.t
   | SelectAll
-  | SelectAllParallel
 
 type goal_identifier = string
 type scope_name = string
@@ -363,7 +362,6 @@ type vernac_expr =
 
   (* Solving *)
 
-  | VernacSolve of goal_selector * int option * raw_tactic_expr * bool
   | VernacSolveExistential of int * constr_expr
 
   (* Auxiliary file and library management *)
diff --git a/parsing/g_ltac.ml4 b/parsing/g_ltac.ml4
index e4ca936a69..79392195fb 100644
--- a/parsing/g_ltac.ml4
+++ b/parsing/g_ltac.ml4
@@ -6,6 +6,9 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+(*i camlp4deps: "grammar/grammar.cma" i*)
+
+open Util
 open Pp
 open Compat
 open Constrexpr
@@ -36,11 +39,42 @@ let reference_to_id = function
       Errors.user_err_loc (loc, "",
         str "This expression should be a simple identifier.")
 
+let tactic_mode = Gram.entry_create "vernac:tactic_command"
+
+let new_entry name =
+  let e = Gram.entry_create name in
+  let entry = Entry.create name in
+  let () = Pcoq.set_grammar entry e in
+  e
+
+let selector = new_entry "vernac:selector"
+
+(* Registers the Classic Proof Mode (which uses [tactic_mode] as a parser for
+    proof editing and changes nothing else). Then sets it as the default proof mode. *)
+let _ =
+  let mode = {
+    Proof_global.name = "Classic";
+    set = (fun () -> set_command_entry tactic_mode);
+    reset = (fun () -> set_command_entry Pcoq.Vernac_.noedit_mode);
+  } in
+  Proof_global.register_proof_mode mode
+
+(* Hack to parse "[ id" without dropping [ *)
+let test_bracket_ident =
+  Gram.Entry.of_parser "test_bracket_ident"
+    (fun strm ->
+      match get_tok (stream_nth 0 strm) with
+        | KEYWORD "[" ->
+            (match get_tok (stream_nth 1 strm) with
+              | IDENT _ -> ()
+	      | _ -> raise Stream.Failure)
+	| _ -> raise Stream.Failure)
+
 (* Tactics grammar rules *)
 
 GEXTEND Gram
   GLOBAL: tactic tacdef_body tactic_expr binder_tactic tactic_arg
-          constr_may_eval constr_eval;
+          tactic_mode constr_may_eval constr_eval selector;
 
   tactic_then_last:
     [ [ "|"; lta = LIST0 OPT tactic_expr SEP "|" ->
@@ -262,4 +296,76 @@ GEXTEND Gram
   tactic:
     [ [ tac = tactic_expr -> tac ] ]
   ;
+  selector:
+    [ [ n=natural; ":" -> Vernacexpr.SelectNth n
+      | test_bracket_ident; "["; id = ident; "]"; ":" -> Vernacexpr.SelectId id
+      | IDENT "all" ; ":" -> Vernacexpr.SelectAll ] ]
+  ;
+  tactic_mode:
+    [ [ g = OPT selector; tac = G_vernac.subgoal_command -> tac g ] ]
+  ;
   END
+
+open Stdarg
+open Constrarg
+open Vernacexpr
+open Vernac_classifier
+
+let print_info_trace = ref None
+
+let _ = let open Goptions in declare_int_option {
+  optsync = true;
+  optdepr = false;
+  optname = "print info trace";
+  optkey = ["Info" ; "Level"];
+  optread = (fun () -> !print_info_trace);
+  optwrite = fun n -> print_info_trace := n;
+}
+
+let vernac_solve n info tcom b =
+  let status = Proof_global.with_current_proof (fun etac p ->
+    let with_end_tac = if b then Some etac else None in
+    let global = match n with SelectAll -> true | _ -> false in
+    let info = Option.append info !print_info_trace in
+    let (p,status) =
+      Pfedit.solve n info (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 Vernacentries.command_focus p in
+    p,status) in
+    if not status then Pp.feedback Feedback.AddedAxiom
+
+let pr_ltac_selector = function
+| SelectNth i -> int i ++ str ":"
+| SelectId id -> str "[" ++ Nameops.pr_id id ++ str "]" ++ str ":"
+| SelectAll -> str "all" ++ str ":"
+
+VERNAC ARGUMENT EXTEND ltac_selector PRINTED BY pr_ltac_selector
+| [ selector(s) ] -> [ s ]
+END
+
+let pr_ltac_info n = str "Info" ++ spc () ++ int n
+
+VERNAC ARGUMENT EXTEND ltac_info PRINTED BY pr_ltac_info
+| [ "Info" natural(n) ] -> [ n ]
+END
+
+let pr_ltac_use_default b = if b then str ".." else mt ()
+
+VERNAC ARGUMENT EXTEND ltac_use_default PRINTED BY pr_ltac_use_default
+| [ "." ] -> [ false ]
+| [ "..." ] -> [ true ]
+END
+
+VERNAC tactic_mode EXTEND VernacSolve
+| [ - ltac_selector_opt(g) ltac_info_opt(n) tactic(t) ltac_use_default(def) ] =>
+    [ classify_as_proofstep ] -> [
+    let g = Option.default (Proof_global.get_default_goal_selector ()) g in
+    vernac_solve g n t def
+  ]
+| [ - "par" ":" ltac_info_opt(n) tactic(t) ltac_use_default(def) ] =>
+    [ VtProofStep true, VtLater ] -> [
+    vernac_solve SelectAll n t def
+  ]
+END
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 49baeb5560..c89238d296 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -34,8 +34,6 @@ let _ = List.iter Lexer.add_keyword vernac_kw
 
 let query_command = Gram.entry_create "vernac:query_command"
 
-let tactic_mode = Gram.entry_create "vernac:tactic_command"
-let noedit_mode = Gram.entry_create "vernac:noedit_command"
 let subprf = Gram.entry_create "vernac:subprf"
 
 let class_rawexpr = Gram.entry_create "vernac:class_rawexpr"
@@ -48,21 +46,6 @@ let subgoal_command = Gram.entry_create "proof_mode:subgoal_command"
 let instance_name = Gram.entry_create "vernac:instance_name"
 let section_subset_expr = Gram.entry_create "vernac:section_subset_expr"
 
-let command_entry = ref noedit_mode
-let set_command_entry e = command_entry := e
-let get_command_entry () = !command_entry
-
-
-(* Registers the Classic Proof Mode (which uses [tactic_mode] as a parser for
-    proof editing and changes nothing else). Then sets it as the default proof mode. *)
-let set_tactic_mode () = set_command_entry tactic_mode
-let set_noedit_mode () = set_command_entry noedit_mode
-let _ = Proof_global.register_proof_mode {Proof_global.
-					    name = "Classic" ;
-					    set = set_tactic_mode ;
-					    reset = set_noedit_mode
-					 }
-
 let make_bullet s =
   let n = String.length s in
   match s.[0] with
@@ -71,23 +54,8 @@ let make_bullet s =
   | '*' -> Star n
   | _ -> assert false
 
-(* Hack to parse "[ id" without dropping [ *)
-let test_bracket_ident =
-  Gram.Entry.of_parser "test_bracket_ident"
-    (fun strm ->
-      match get_tok (stream_nth 0 strm) with
-        | KEYWORD "[" ->
-            (match get_tok (stream_nth 1 strm) with
-              | IDENT _ -> ()
-	      | _ -> raise Stream.Failure)
-	| _ -> raise Stream.Failure)
-
-let default_command_entry =
-  Gram.Entry.of_parser "command_entry"
-    (fun strm -> Gram.parse_tokens_after_filter (get_command_entry ()) strm)
-
 GEXTEND Gram
-  GLOBAL: vernac gallina_ext tactic_mode noedit_mode subprf subgoal_command;
+  GLOBAL: vernac gallina_ext noedit_mode subprf subgoal_command;
   vernac: FIRST
     [ [ IDENT "Time"; c = located_vernac -> VernacTime c
       | IDENT "Redirect"; s = ne_string; c = located_vernac -> VernacRedirect (s, c)
@@ -129,24 +97,12 @@ GEXTEND Gram
     ] ]
   ;
   vernac_aux: LAST
-    [ [ prfcom = default_command_entry -> prfcom ] ]
+    [ [ prfcom = command_entry -> prfcom ] ]
   ;
   noedit_mode:
     [ [ c = subgoal_command -> c None] ]
   ;
 
-  selector:
-    [ [ n=natural; ":" -> SelectNth n
-      | test_bracket_ident; "["; id = ident; "]"; ":" -> SelectId id
-      | IDENT "all" ; ":" -> SelectAll
-      | IDENT "par" ; ":" -> SelectAllParallel ] ]
-  ;
-
-  tactic_mode:
-  [ [ gln = OPT selector;
-      tac = subgoal_command -> tac gln ] ]
-  ;
-
   subprf:
   [ [ s = BULLET -> VernacBullet (make_bullet s)
     | "{" -> VernacSubproof None
@@ -161,13 +117,7 @@ GEXTEND Gram
                     | None -> c None
                     | _ ->
                         VernacError (UserError ("",str"Typing and evaluation commands, cannot be used with the \"all:\" selector."))
-                  end
-      | info = OPT [IDENT "Info";n=natural -> n];
-        tac = Tactic.tactic;
-        use_dft_tac = [ "." -> false | "..." -> true ] ->
-        (fun g ->
-            let g = Option.default (Proof_global.get_default_goal_selector ()) g in
-            VernacSolve(g,info,tac,use_dft_tac)) ] ]
+                  end ] ]
   ;
   located_vernac:
     [ [ v = vernac -> !@loc, v ] ]
diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml
index 91f933987b..9c2f09db84 100644
--- a/parsing/pcoq.ml
+++ b/parsing/pcoq.ml
@@ -383,6 +383,7 @@ module Vernac_ =
     let rec_definition = gec_vernac "Vernac.rec_definition"
     (* Main vernac entry *)
     let main_entry = Gram.entry_create "vernac"
+    let noedit_mode = gec_vernac "noedit_command"
 
     let () =
       let act_vernac = Gram.action (fun v loc -> Some (!@loc, v)) in
@@ -393,10 +394,18 @@ module Vernac_ =
       ] in
       maybe_uncurry (Gram.extend main_entry) (None, make_rule rule)
 
+    let command_entry_ref = ref noedit_mode
+    let command_entry =
+      Gram.Entry.of_parser "command_entry"
+        (fun strm -> Gram.parse_tokens_after_filter !command_entry_ref strm)
+
   end
 
 let main_entry = Vernac_.main_entry
 
+let set_command_entry e = Vernac_.command_entry_ref := e
+let get_command_entry () = !Vernac_.command_entry_ref
+
 (**********************************************************************)
 (* This determines (depending on the associativity of the current
    level and on the expected associativity) if a reference to constr_n is
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index d6bfe3eb39..7410d4e44c 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -241,11 +241,17 @@ module Vernac_ :
     val vernac : vernac_expr Gram.entry
     val rec_definition : (fixpoint_expr * decl_notation list) Gram.entry
     val vernac_eoi : vernac_expr Gram.entry
+    val noedit_mode : vernac_expr Gram.entry
+    val command_entry : vernac_expr Gram.entry
   end
 
 (** The main entry: reads an optional vernac command *)
 val main_entry : (Loc.t * vernac_expr) option Gram.entry
 
+(** Handling of the proof mode entry *)
+val get_command_entry : unit -> vernac_expr Gram.entry
+val set_command_entry : vernac_expr Gram.entry -> unit
+
 (** Mapping formal entries into concrete ones *)
 
 (** Binding constr entry keys to entries and symbols *)
diff --git a/plugins/decl_mode/g_decl_mode.ml4 b/plugins/decl_mode/g_decl_mode.ml4
index 2afbaca2c8..a438ca79f4 100644
--- a/plugins/decl_mode/g_decl_mode.ml4
+++ b/plugins/decl_mode/g_decl_mode.ml4
@@ -135,7 +135,7 @@ let _ =
 				       set = begin fun () ->
 					 (* We set the command non terminal to
 					     [proof_mode] (which we just defined). *)
-					 G_vernac.set_command_entry proof_mode ;
+					 Pcoq.set_command_entry proof_mode ;
 					 (* We substitute the goal printer, by the one we built
 					     for the proof mode. *)
 					 Printer.set_printer_pr { Printer.default_printer_pr with
@@ -147,7 +147,7 @@ let _ =
 				       reset = begin fun () ->
 					 (* We restore the command non terminal to
 					      [noedit_mode]. *)
-					 G_vernac.set_command_entry G_vernac.noedit_mode ;
+					 Pcoq.set_command_entry Pcoq.Vernac_.noedit_mode ;
 					 (* We restore the goal printer to default *)
 					 Printer.set_printer_pr Printer.default_printer_pr
 				       end
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index a101540aba..887a14d2bf 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -979,24 +979,6 @@ module Make
                      prlist_with_sep (fun () -> str " <+ ") pr_m mexprs)
           )
         (* Solving *)
-      | VernacSolve (i,info,tac,deftac) ->
-        let pr_goal_selector = function
-          | SelectNth i -> int i ++ str":"
-          | SelectId id -> pr_id id ++ str":"
-          | SelectAll -> str"all" ++ str":"
-          | SelectAllParallel -> str"par"
-        in
-        let pr_info =
-          match info with
-            | None -> mt ()
-            | Some i -> str"Info"++spc()++int i++spc()
-        in
-        return (
-          (if i = Proof_global.get_default_goal_selector () then mt() else pr_goal_selector i) ++
-          pr_info ++
-          pr_raw_tactic tac
-          ++ (if deftac then str ".." else mt ())
-        )
         | VernacSolveExistential (i,c) ->
           return (keyword "Existential" ++ spc () ++ int i ++ pr_lconstrarg c)
 
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index 20d696fd91..608ee2c700 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -105,8 +105,6 @@ let solve ?with_end_tac gi info_lvl tac pr =
       | Vernacexpr.SelectNth i -> Proofview.tclFOCUS i i tac
       | Vernacexpr.SelectId id -> Proofview.tclFOCUSID id tac
       | Vernacexpr.SelectAll -> tac
-      | Vernacexpr.SelectAllParallel ->
-          Errors.anomaly(str"SelectAllParallel not handled by Stm")
     in
     let (p,(status,info)) = Proof.run_tactic (Global.env ()) tac pr in
     let () =
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index d19dc5ba0f..647dbe1115 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -664,7 +664,6 @@ let print_goal_selector = function
   | Vernacexpr.SelectAll -> "all"
   | Vernacexpr.SelectNth i -> string_of_int i
   | Vernacexpr.SelectId id -> Id.to_string id
-  | Vernacexpr.SelectAllParallel -> "par"
 
 let parse_goal_selector = function
   | "all" -> Vernacexpr.SelectAll
diff --git a/stm/stm.ml b/stm/stm.ml
index 07262ef68f..92032e9bc3 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -1140,9 +1140,10 @@ end = struct (* {{{ *)
   
   let perform_states query =
     if query = [] then [] else
-    let is_tac = function
-      | VernacSolve _ | VernacFocus _ | VernacUnfocus | VernacBullet _ -> true
-      | _ -> false in
+    let is_tac e = match classify_vernac e with
+    | VtProofStep _, _ -> true
+    | _ -> false
+    in
     let initial = 
       let rec aux id =
         try match VCS.visit id with { next } -> aux next
@@ -1413,7 +1414,7 @@ and TacTask : sig
     t_state    : Stateid.t;
     t_state_fb : Stateid.t;
     t_assign   : output Future.assignement -> unit;
-    t_ast      : ast;
+    t_ast      : int * ast;
     t_goal     : Goal.goal;
     t_kill     : unit -> unit;
     t_name     : string }  
@@ -1430,7 +1431,7 @@ end = struct (* {{{ *)
     t_state    : Stateid.t;
     t_state_fb : Stateid.t;
     t_assign   : output Future.assignement -> unit;
-    t_ast      : ast;
+    t_ast      : int * ast;
     t_goal     : Goal.goal;
     t_kill     : unit -> unit;
     t_name     : string }  
@@ -1439,7 +1440,7 @@ end = struct (* {{{ *)
     r_state    : Stateid.t;
     r_state_fb : Stateid.t;
     r_document : VCS.vcs option;
-    r_ast      : ast;
+    r_ast      : int * ast;
     r_goal     : Goal.goal;
     r_name     : string }
 
@@ -1483,6 +1484,9 @@ end = struct (* {{{ *)
     | Some { t_kill } -> t_kill ()
     | _ -> ()
  
+  let command_focus = Proof.new_focus_kind ()
+  let focus_cond = Proof.no_cond command_focus
+
   let perform { r_state = id; r_state_fb; r_document = vcs; r_ast; r_goal } =
     Option.iter VCS.restore vcs;
     try
@@ -1498,7 +1502,9 @@ end = struct (* {{{ *)
          Errors.errorlabstrm "Stm" (strbrk("the par: goal selector supports ground "^
            "goals only"))
        else begin
-        vernac_interp r_state_fb r_ast;
+        let (i, ast) = r_ast in
+        Proof_global.simple_with_current_proof (fun _ p -> Proof.focus focus_cond () i p);
+        vernac_interp r_state_fb ast;
         let _,_,_,_,sigma = Proof.proof (Proof_global.give_me_the_proof ()) in
         match Evd.(evar_body (find sigma r_goal)) with
         | Evd.Evar_empty -> Errors.errorlabstrm "Stm" (str "no progress")
@@ -1527,12 +1533,11 @@ end = struct (* {{{ *)
   module TaskQueue = AsyncTaskQueue.MakeQueue(TacTask)
 
   let vernac_interp cancel nworkers safe_id id { verbose; loc; expr = e } =
-    let e, etac, time, fail =
+    let e, time, fail =
       let rec find time fail = function
-        | VernacSolve(_,_,re,b) -> re, b, time, fail
         | VernacTime (_,e) | VernacRedirect (_,(_,e)) -> find true fail e
         | VernacFail e -> find time true e
-        | _ -> errorlabstrm "Stm" (str"unsupported") in find false false e in
+        | _ -> e, time, fail in find false false e in
     Hooks.call Hooks.with_fail fail (fun () ->
     (if time then System.with_time false else (fun x -> x)) (fun () ->
     ignore(TaskQueue.with_n_workers nworkers (fun queue ->
@@ -1544,8 +1549,7 @@ end = struct (* {{{ *)
           Future.create_delegate
             ~name:(Printf.sprintf "subgoal %d" i)
             (State.exn_on id ~valid:safe_id) in
-        let t_ast =
-          { verbose;loc;expr = VernacSolve(SelectNth i,None,e,etac) } in
+        let t_ast = (i, { verbose; loc; expr = e }) in
         let t_name = Goal.uid g in
         TaskQueue.enqueue_task queue
           ({ t_state = safe_id; t_state_fb = id;
diff --git a/stm/texmacspp.ml b/stm/texmacspp.ml
index 3c4b8cb71e..a459cd65f8 100644
--- a/stm/texmacspp.ml
+++ b/stm/texmacspp.ml
@@ -671,7 +671,7 @@ let rec tmpp v loc =
 
   (* Solving *)
 
-  | (VernacSolve _ | VernacSolveExistential _) as x ->
+  | (VernacSolveExistential _) as x ->
       xmlLtac loc [PCData (Pp.string_of_ppcmds (Ppvernac.pr_vernac x))]
 
   (* Auxiliary file and library management *)
diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml
index f9f08f7afb..97d6e1fb71 100644
--- a/stm/vernac_classifier.ml
+++ b/stm/vernac_classifier.ml
@@ -102,12 +102,10 @@ let rec classify_vernac e =
     | VernacCheckMayEval _ ->
         VtQuery (true,(Stateid.dummy,Feedback.default_route)), VtLater
     (* ProofStep *)
-    | VernacSolve (SelectAllParallel,_,_,_) -> VtProofStep true, VtLater
     | VernacProof _ 
     | VernacBullet _ 
     | VernacFocus _ | VernacUnfocus
     | VernacSubproof _ | VernacEndSubproof
-    | VernacSolve _ 
     | VernacCheckGuard
     | VernacUnfocused
     | VernacSolveExistential _ -> VtProofStep false, VtLater
diff --git a/test-suite/bugs/opened/3410.v b/test-suite/bugs/opened/3410.v
deleted file mode 100644
index 0d259181aa..0000000000
--- a/test-suite/bugs/opened/3410.v
+++ /dev/null
@@ -1 +0,0 @@
-Fail repeat match goal with H:_ |- _ => setoid_rewrite X in H end.
diff --git a/test-suite/ide/undo013.fake b/test-suite/ide/undo013.fake
index f44156aa38..921a9d0f0d 100644
--- a/test-suite/ide/undo013.fake
+++ b/test-suite/ide/undo013.fake
@@ -23,5 +23,5 @@ ADD { Qed. }
 ADD { apply H. }
 # </replay>
 ADD { Qed. }
-QUERY { Fail idtac. }
+QUERY { Fail Show. }
 QUERY { Check (aa,bb,cc). }
diff --git a/test-suite/ide/undo014.fake b/test-suite/ide/undo014.fake
index 6d58b061e6..f5fe774704 100644
--- a/test-suite/ide/undo014.fake
+++ b/test-suite/ide/undo014.fake
@@ -22,5 +22,5 @@ ADD { destruct H. }
 ADD { Qed. }
 ADD { apply H. }
 ADD { Qed. }
-QUERY { Fail idtac. }
+QUERY { Fail Show. }
 QUERY { Check (aa,bb,cc). }
diff --git a/test-suite/ide/undo015.fake b/test-suite/ide/undo015.fake
index ac17985aab..a1e5c947b3 100644
--- a/test-suite/ide/undo015.fake
+++ b/test-suite/ide/undo015.fake
@@ -25,5 +25,5 @@ ADD { destruct H. }
 ADD { Qed. }
 ADD { apply H. }
 ADD { Qed. }
-QUERY { Fail idtac. }
+QUERY { Fail Show. }
 QUERY { Check (aa,bb,cc). }
diff --git a/test-suite/ide/undo016.fake b/test-suite/ide/undo016.fake
index bdb81ecd95..f9414c1ea7 100644
--- a/test-suite/ide/undo016.fake
+++ b/test-suite/ide/undo016.fake
@@ -27,5 +27,5 @@ ADD { destruct H. }
 ADD { Qed. }
 ADD { apply H. }
 ADD { Qed. }
-QUERY { Fail idtac. }
+QUERY { Fail Show. }
 QUERY { Check (aa,bb,cc). }
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 02f8c17175..8ba5eb3f7d 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -826,35 +826,6 @@ let vernac_declare_class id =
 let command_focus = Proof.new_focus_kind ()
 let focus_command_cond = Proof.no_cond command_focus
 
-
-let print_info_trace = ref None
-
-let _ = let open Goptions in declare_int_option {
-  optsync = true;
-  optdepr = false;
-  optname = "print info trace";
-  optkey = ["Info" ; "Level"];
-  optread = (fun () -> !print_info_trace);
-  optwrite = fun n -> print_info_trace := n;
-}
-
-let vernac_solve n info tcom b =
-  if not (refining ()) then
-    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 global = match n with SelectAll -> true | _ -> false in
-    let info = Option.append info !print_info_trace in
-    let (p,status) =
-      solve n info (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
-    p,status) in
-    if not status then Pp.feedback Feedback.AddedAxiom
- 
-
   (* A command which should be a tactic. It has been
      added by Christine to patch an error in the design of the proof
      machine, and enables to instantiate existential variables when
@@ -884,14 +855,13 @@ let vernac_set_used_variables e =
         (str "Unknown variable: " ++ pr_id id))
     l;
   let _, to_clear = set_used_variables l in
-  (** FIXME: too fragile *)
-  let open Tacexpr in
-  let tac = { mltac_plugin = "coretactics"; mltac_tactic = "clear" } in
-  let tac = { mltac_name = tac; mltac_index = 0 } in
-  let arg = Genarg.in_gen (Genarg.rawwit (Genarg.wit_list Constrarg.wit_var)) to_clear in
-  let tac = if List.is_empty to_clear then TacId [] else TacML (Loc.ghost, tac, [TacGeneric arg]) in
-  vernac_solve SelectAll None tac false
-
+  let to_clear = List.map snd to_clear in
+  Proof_global.with_current_proof begin fun _ p ->
+    if List.is_empty to_clear then (p, ())
+    else
+      let tac = Proofview.V82.tactic (Tactics.clear to_clear) in
+      fst (solve SelectAll None tac p), ()
+  end
 
 (*****************************)
 (* Auxiliary file management *)
@@ -1909,7 +1879,6 @@ let interp ?proof ~loc locality poly c =
   | VernacDeclareClass id -> vernac_declare_class id
 
   (* Solving *)
-  | VernacSolve (n,info,tac,b) -> vernac_solve n info tac b
   | VernacSolveExistential (n,c) -> vernac_solve_existential n c
 
   (* Auxiliary file and library management *)
diff --git a/toplevel/vernacentries.mli b/toplevel/vernacentries.mli
index 451ccdb4d4..4a59b1299b 100644
--- a/toplevel/vernacentries.mli
+++ b/toplevel/vernacentries.mli
@@ -59,3 +59,5 @@ val vernac_end_proof :
   ?proof:Proof_global.closed_proof -> Vernacexpr.proof_end -> unit
 
 val with_fail : bool -> (unit -> unit) -> unit
+
+val command_focus : unit Proof.focus_kind