Imported Upstream version 8.2~beta3+dfsgupstream/8.2.beta3+dfsg

1 files changed, 23 insertions, 0 deletions

diff --git a/test-suite/success/Discriminate.v b/test-suite/success/Discriminate.v
index f28c83de..b57c5478 100644
--- a/test-suite/success/Discriminate.v
+++ b/test-suite/success/Discriminate.v
@@ -9,3 +9,26 @@ Qed.
 Lemma l2 : forall H : 0 = 1, H = H.   
  discriminate H.
 Qed.
+
+(* Check the variants of discriminate *)
+
+Goal O = S O -> True.
+discriminate 1.
+Undo.
+intros.
+discriminate H.
+Undo.
+Ltac g x := discriminate x.
+g H.
+Abort.
+
+Goal (forall x y : nat, x = y -> x = S y) -> True.
+intros.
+try discriminate (H O) || exact I.
+Qed.
+
+Goal (forall x y : nat, x = y -> x = S y) -> True.
+intros.
+ediscriminate (H O).
+instantiate (1:=O).
+Abort.