This problem is partly related to coq/7922. In that issue, a hack is proposed to convert strings to idents by using ltac2. However, I’m not quite sure how to do it in the reversed way (say, converting idents to strings).
More specifically, I’m trying to do something like
(fun (x y: ty) => ...) with
Goal True. Proof. match constr:((fun (x y: nat) => x)) with | (fun (name:_) => _) => some_tac (ident_to_string name) end.
Now I have an intropattern
idtac name prints
x. The problem is, this
some_tac can only accept a string. Is there any way to write a
ident_to_string ltac to magically acquire string