Binder.make
is the most painful part of the Ltac2 Unsafe Constr API, and I continue to be very frustrated with it and the way it will quite easily raise typechecking anomalies (in a part of the code that's not supposed to be doing any typechecking)
Yes, there should be an even lower-level API as it used to be.
Last updated: May 28 2023 at 16:30 UTC