blob: f22a8cccc5e90a5bbd048db7ee5d7b1dc1148dd3 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
|
(* Check correct behavior of add_primitive_tactic in TACEXTEND *)
(* Added also the case of eauto and congruence *)
Ltac thus H := solve [H].
Lemma test: forall n : nat, n <= n.
Proof.
intro.
thus firstorder.
Undo.
thus eauto.
Qed.
Lemma test2: false = true -> False.
Proof.
intro.
thus congruence.
Qed.
|
