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.
Tactic Definition titi:=Auto.
End toto.

Module ti.
Import toto.
Tactic Definition equal:=
Match Context With
[ |- ?1=?1]-> titi
| [ |- ?]-> Idtac.

End ti.

Import ti.
Definition simple:(a:nat) a=a.
Intro.
equal.
Qed.