Library Ltac2.Ident

Require Import Ltac2.Init.

Ltac2 Type t := ident.

Ltac2 @ external equal : t -> t -> bool := "coq-core.plugins.ltac2" "ident_equal".

Ltac2 @ external of_string : string -> t option := "coq-core.plugins.ltac2" "ident_of_string".

Ltac2 @ external to_string : t -> string := "coq-core.plugins.ltac2" "ident_to_string".