Require Import Ltac2.Init.
Ltac2
Type t :=
ident.
Ltac2 @
external equal :
t ->
t ->
bool := "ltac2" "ident_equal".
Ltac2 @
external of_string :
string ->
t option := "ltac2" "ident_of_string".
Ltac2 @
external to_string :
t ->
string := "ltac2" "ident_to_string".