From ce2ffd090bd64963279cbbb84012d1b266ed9918 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sat, 19 Mar 2016 01:43:29 +0100
Subject: Moving VernacSolve to an EXTEND-based definition.

---
 printing/ppvernac.ml | 18 ------------------
 1 file changed, 18 deletions(-)

(limited to 'printing')

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)
 
-- 
cgit v1.2.3