From f1a561d847e207433a0ec3e6333798dfa19e4a0c Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 17 Sep 2016 20:24:36 +0200
Subject: Further "decide equality" tests on demand of Jason.

---
 test-suite/success/eqdecide.v | 12 ++++++++++++
 1 file changed, 12 insertions(+)

(limited to 'test-suite')

diff --git a/test-suite/success/eqdecide.v b/test-suite/success/eqdecide.v
index 1f6af0dc44..724e2998ef 100644
--- a/test-suite/success/eqdecide.v
+++ b/test-suite/success/eqdecide.v
@@ -14,6 +14,18 @@ Lemma lem1 : forall x y : T, {x = y} + {x <> y}.
  decide equality.
 Qed.
 
+Lemma lem1' : forall x y : T, x = y \/ x <> y.
+ decide equality.
+Qed.
+
+Lemma lem1'' : forall x y : T, {x <> y} + {x = y}.
+ decide equality.
+Qed.
+
+Lemma lem1''' : forall x y : T, x <> y \/ x = y.
+ decide equality.
+Qed.
+
 Lemma lem2 : forall x y : T, {x = y} + {x <> y}.
 intros x y.
  decide equality.
-- 
cgit v1.2.3