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.

1 files changed, 0 insertions, 18 deletions

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)