From 753248c145cdac846528d809a1f085c18408e17f Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 15 Sep 2016 19:30:45 +0200
Subject: Added a test file for contradiction.

---
 test-suite/success/contradiction.v | 32 ++++++++++++++++++++++++++++++++
 1 file changed, 32 insertions(+)
 create mode 100644 test-suite/success/contradiction.v

diff --git a/test-suite/success/contradiction.v b/test-suite/success/contradiction.v
new file mode 100644
index 0000000000..92a7c6ccbc
--- /dev/null
+++ b/test-suite/success/contradiction.v
@@ -0,0 +1,32 @@
+(* Some tests for contradiction *)
+
+Lemma L1 : forall A B : Prop, A -> ~A -> B.
+Proof.
+intros; contradiction.
+Qed.
+
+Lemma L2 : forall A B : Prop, ~A -> A -> B.
+Proof.
+intros; contradiction.
+Qed.
+
+Lemma L3 : forall A : Prop, ~True -> A.
+Proof.
+intros; contradiction.
+Qed.
+
+Lemma L4 : forall A : Prop, forall x : nat, ~x=x -> A.
+Proof.
+intros; contradiction.
+Qed.
+
+Lemma L5 : forall A : Prop, forall x y : nat, ~x=y -> x=y -> A.
+Proof.
+intros; contradiction.
+Qed.
+
+Lemma L6 : forall A : Prop, forall x y : nat, x=y -> ~x=y -> A.
+Proof.
+intros; contradiction.
+Qed.
+
-- 
cgit v1.2.3