test-suite/success/Mod_ltac.v


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.