aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/success/eqdecide.v
diff options
context:
space:
mode:
Diffstat (limited to 'test-suite/success/eqdecide.v')
-rw-r--r--test-suite/success/eqdecide.v12
1 files changed, 12 insertions, 0 deletions
diff --git a/test-suite/success/eqdecide.v b/test-suite/success/eqdecide.v
index 1f6af0dc4..724e2998e 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.