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.

---
 stm/texmacspp.ml         | 2 +-
 stm/vernac_classifier.ml | 2 --
 2 files changed, 1 insertion(+), 3 deletions(-)

(limited to 'stm')

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