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.

5 files changed, 4 insertions, 5 deletions

diff --git a/test-suite/bugs/opened/3410.v b/test-suite/bugs/opened/3410.v
deleted file mode 100644
index 0d259181aa..0000000000
--- a/test-suite/bugs/opened/3410.v
+++ /dev/null
@@ -1 +0,0 @@
-Fail repeat match goal with H:_ |- _ => setoid_rewrite X in H end.
diff --git a/test-suite/ide/undo013.fake b/test-suite/ide/undo013.fake
index f44156aa38..921a9d0f0d 100644
--- a/test-suite/ide/undo013.fake
+++ b/test-suite/ide/undo013.fake
@@ -23,5 +23,5 @@ ADD { Qed. }
 ADD { apply H. }
 # </replay>
 ADD { Qed. }
-QUERY { Fail idtac. }
+QUERY { Fail Show. }
 QUERY { Check (aa,bb,cc). }
diff --git a/test-suite/ide/undo014.fake b/test-suite/ide/undo014.fake
index 6d58b061e6..f5fe774704 100644
--- a/test-suite/ide/undo014.fake
+++ b/test-suite/ide/undo014.fake
@@ -22,5 +22,5 @@ ADD { destruct H. }
 ADD { Qed. }
 ADD { apply H. }
 ADD { Qed. }
-QUERY { Fail idtac. }
+QUERY { Fail Show. }
 QUERY { Check (aa,bb,cc). }
diff --git a/test-suite/ide/undo015.fake b/test-suite/ide/undo015.fake
index ac17985aab..a1e5c947b3 100644
--- a/test-suite/ide/undo015.fake
+++ b/test-suite/ide/undo015.fake
@@ -25,5 +25,5 @@ ADD { destruct H. }
 ADD { Qed. }
 ADD { apply H. }
 ADD { Qed. }
-QUERY { Fail idtac. }
+QUERY { Fail Show. }
 QUERY { Check (aa,bb,cc). }
diff --git a/test-suite/ide/undo016.fake b/test-suite/ide/undo016.fake
index bdb81ecd95..f9414c1ea7 100644
--- a/test-suite/ide/undo016.fake
+++ b/test-suite/ide/undo016.fake
@@ -27,5 +27,5 @@ ADD { destruct H. }
 ADD { Qed. }
 ADD { apply H. }
 ADD { Qed. }
-QUERY { Fail idtac. }
+QUERY { Fail Show. }
 QUERY { Check (aa,bb,cc). }