coq-elpi icon indicating copy to clipboard operation
coq-elpi copied to clipboard
verified publisher icon LPCIC

Name holes in detyping

Open Tragicus opened this issue 1 month ago • 7 comments

src/rocq_elpi_utils.ml/detype now turns identical evars into identical holes. Fixes #919

Tragicus avatar Nov 06 '25 14:11 Tragicus