Ltac bug_13004.t := ltac2:(print (of_string "hi"))
Ltac bug_13004.u := ident:(H)