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: Nov 29 2023 at 19:01 UTC