From b17a1c36621cba0774713ff63e0cff64eccfc085 Mon Sep 17 00:00:00 2001
From: augustin64 <me.git@augustin64.fr>
Date: Mon, 20 May 2024 11:13:28 +0200
Subject: [PATCH] Add more bad 8pus tests

---
 tests/8pus/bad/no_arg_tactic.8pus  | 6 ++++++
 tests/8pus/bad/not_yet_qed.8pus    | 4 ++++
 tests/8pus/bad/undo_empty.8pus     | 1 +
 tests/8pus/bad/undo_loop.8pus      | 6 ++++++
 tests/8pus/bad/undo_qed.8pus       | 7 +++++++
 tests/8pus/bad/undo_try.8pus       | 7 +++++++
 tests/8pus/bad/unknown_tactic.8pus | 2 ++
 tests/8pus/bad/unkown_try.8pus     | 3 +++
 8 files changed, 36 insertions(+)
 create mode 100644 tests/8pus/bad/no_arg_tactic.8pus
 create mode 100644 tests/8pus/bad/not_yet_qed.8pus
 create mode 100644 tests/8pus/bad/undo_empty.8pus
 create mode 100644 tests/8pus/bad/undo_loop.8pus
 create mode 100644 tests/8pus/bad/undo_qed.8pus
 create mode 100644 tests/8pus/bad/undo_try.8pus
 create mode 100644 tests/8pus/bad/unknown_tactic.8pus
 create mode 100644 tests/8pus/bad/unkown_try.8pus

diff --git a/tests/8pus/bad/no_arg_tactic.8pus b/tests/8pus/bad/no_arg_tactic.8pus
new file mode 100644
index 0000000..4ac19d8
--- /dev/null
+++ b/tests/8pus/bad/no_arg_tactic.8pus
@@ -0,0 +1,6 @@
+Goal A -> B -> C -> A.
+intros.
+    apply.
+    exact.
+assumption.
+Qed.
\ No newline at end of file
diff --git a/tests/8pus/bad/not_yet_qed.8pus b/tests/8pus/bad/not_yet_qed.8pus
new file mode 100644
index 0000000..c0b7a3f
--- /dev/null
+++ b/tests/8pus/bad/not_yet_qed.8pus
@@ -0,0 +1,4 @@
+Goal A -> B -> A.
+intros.
+Qed.
+Check.
\ No newline at end of file
diff --git a/tests/8pus/bad/undo_empty.8pus b/tests/8pus/bad/undo_empty.8pus
new file mode 100644
index 0000000..025c002
--- /dev/null
+++ b/tests/8pus/bad/undo_empty.8pus
@@ -0,0 +1 @@
+Undo.
\ No newline at end of file
diff --git a/tests/8pus/bad/undo_loop.8pus b/tests/8pus/bad/undo_loop.8pus
new file mode 100644
index 0000000..c82db5e
--- /dev/null
+++ b/tests/8pus/bad/undo_loop.8pus
@@ -0,0 +1,6 @@
+Goal A -> B.
+intro.
+Undo.
+Undo.
+Undo.
+Undo.
\ No newline at end of file
diff --git a/tests/8pus/bad/undo_qed.8pus b/tests/8pus/bad/undo_qed.8pus
new file mode 100644
index 0000000..5a58867
--- /dev/null
+++ b/tests/8pus/bad/undo_qed.8pus
@@ -0,0 +1,7 @@
+Goal (A -> B) -> A -> B.
+intros.
+apply H0.
+exact H1.
+Qed.
+Undo.
+Qed.
\ No newline at end of file
diff --git a/tests/8pus/bad/undo_try.8pus b/tests/8pus/bad/undo_try.8pus
new file mode 100644
index 0000000..549111d
--- /dev/null
+++ b/tests/8pus/bad/undo_try.8pus
@@ -0,0 +1,7 @@
+Goal A -> B -> A.
+intros.
+try intro.
+Undo.
+intro.
+exact H0.
+Qed.
\ No newline at end of file
diff --git a/tests/8pus/bad/unknown_tactic.8pus b/tests/8pus/bad/unknown_tactic.8pus
new file mode 100644
index 0000000..d330417
--- /dev/null
+++ b/tests/8pus/bad/unknown_tactic.8pus
@@ -0,0 +1,2 @@
+Goal A -> B.
+ancienttactic.
\ No newline at end of file
diff --git a/tests/8pus/bad/unkown_try.8pus b/tests/8pus/bad/unkown_try.8pus
new file mode 100644
index 0000000..931350f
--- /dev/null
+++ b/tests/8pus/bad/unkown_try.8pus
@@ -0,0 +1,3 @@
+Goal A -> B -> C -> A.
+intros.
+try autosolve.
\ No newline at end of file