1
(* Check the behaviour of Discriminate *)
3
(* Check that Discriminate tries Intro until *)
5
Lemma l1 : 0 = 1 -> False.
9
Lemma l2 : forall H : 0 = 1, H = H.
13
(* Check the variants of discriminate *)
21
Ltac g x := discriminate x.
25
Goal (forall x y : nat, x = y -> x = S y) -> True.
27
try discriminate (H O) || exact I.
30
Goal (forall x y : nat, x = y -> x = S y) -> True.