test: Add tests and some fix

1 files changed, 12 insertions, 2 deletions

diff --git a/ci/test1.v b/ci/test1.v
index fc1fc943..3812adbd 100644
--- a/ci/test1.v
+++ b/ci/test1.v
@@ -1,7 +1,7 @@
 Definition trois := 3. (*test-definition*)
 Print trois.
 Eval compute in 10 * trois * trois.
-
+ 
 
 
 Lemma easy_proof : forall A : Prop, A -> A.
@@ -9,4 +9,14 @@ Proof using .
   intros A.
   intros proof_of_A. (*test-insert*)
   exact proof_of_A.
-Qed. (*test-lemma*) 
+Qed. (*test-lemma*)
+
+Lemma false_proof : forall A B : bool, A = B. 
+Proof.
+  intros A B.
+  destruct A.
+  destruct B.
+  reflexivity. (*error*)
+  reflexivity.
+Qed. (*test-lemma2*)
+