blob: 1a9f6fc53c1ca3a2098c55e8b169c27651d9e9aa (
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.
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.
|
