From 6313af9346a624ef2de5b0624036d279a2d23c4e Mon Sep 17 00:00:00 2001
From: augustin64 <me.git@augustin64.fr>
Date: Mon, 20 May 2024 14:52:19 +0200
Subject: [PATCH] Add more bad 8pus tests

---
 tests/8pus/bad/badHtype_exact.8pus | 5 +++++
 tests/8pus/bad/badtype_exact.8pus  | 7 ++-----
 tests/8pus/bad/notype_exact.8pus   | 2 ++
 3 files changed, 9 insertions(+), 5 deletions(-)
 create mode 100644 tests/8pus/bad/badHtype_exact.8pus
 create mode 100644 tests/8pus/bad/notype_exact.8pus

diff --git a/tests/8pus/bad/badHtype_exact.8pus b/tests/8pus/bad/badHtype_exact.8pus
new file mode 100644
index 0000000..a4271ce
--- /dev/null
+++ b/tests/8pus/bad/badHtype_exact.8pus
@@ -0,0 +1,5 @@
+Goal A -> B -> A.
+intro.
+exact H1.
+exact H0.
+Qed.
\ No newline at end of file
diff --git a/tests/8pus/bad/badtype_exact.8pus b/tests/8pus/bad/badtype_exact.8pus
index a4271ce..a0d9348 100644
--- a/tests/8pus/bad/badtype_exact.8pus
+++ b/tests/8pus/bad/badtype_exact.8pus
@@ -1,5 +1,2 @@
-Goal A -> B -> A.
-intro.
-exact H1.
-exact H0.
-Qed.
\ No newline at end of file
+Goal A -> B.
+exact (fun (x:A) => x).
\ No newline at end of file
diff --git a/tests/8pus/bad/notype_exact.8pus b/tests/8pus/bad/notype_exact.8pus
new file mode 100644
index 0000000..86da4e3
--- /dev/null
+++ b/tests/8pus/bad/notype_exact.8pus
@@ -0,0 +1,2 @@
+Goal A -> B.
+exact (fun (x:A) => y).
\ No newline at end of file