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