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.

---
 intf/vernacexpr.mli | 2 --
 1 file changed, 2 deletions(-)

(limited to 'intf')

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