test-suite/output/bug_13004.v


1
2
3
4
5
6
7

Require Import Ltac2.Ltac2 Ltac2.Message.

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

Print t.
Print u.