aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2016-03-19 01:43:29 +0100
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2016-03-19 02:49:03 +0100
commitce2ffd090bd64963279cbbb84012d1b266ed9918 (patch)
tree842afc28f891fa8516cbb86d1051b41686eb67a6 /proofs
parent65e0522033ea47ed479227be30a92fceaa8c6358 (diff)
Moving VernacSolve to an EXTEND-based definition.
Diffstat (limited to 'proofs')
-rw-r--r--proofs/pfedit.ml2
-rw-r--r--proofs/proof_global.ml1
2 files changed, 1 insertions, 2 deletions
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index 0fdcaa587..608ee2c70 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -104,7 +104,7 @@ let solve ?with_end_tac gi info_lvl tac pr =
let tac = match gi with
| Vernacexpr.SelectNth i -> Proofview.tclFOCUS i i tac
| Vernacexpr.SelectId id -> Proofview.tclFOCUSID id tac
- | Vernacexpr.SelectAll | Vernacexpr.SelectAllParallel -> tac
+ | Vernacexpr.SelectAll -> tac
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 d19dc5ba0..647dbe111 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