diff options
Diffstat (limited to 'test-suite/success/Discriminate.v')
| -rw-r--r-- | test-suite/success/Discriminate.v | 23 |
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. |