blob: 44bb3a55ec69842c2d875051ce9d1b1d78c6f8a8 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
|
(* Submitted by Houda Anoun *)
Module toto.
Ltac titi := auto.
End toto.
Module ti.
Import toto.
Ltac equal := match goal with
| |- (?X1 = ?X1) => titi
| |- _ => idtac
end.
End ti.
Import ti.
Definition simple : forall a : nat, a = a.
intro.
equal.
Qed.
|