aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/success/Mod_ltac.v
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.