Jason Gross (Dec 29 2020 at 18:41): Jason Gross (Dec 29 2020 at 18:41):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)
Pierre-Marie Pédrot (Dec 29 2020 at 19:27):Yes, there should be an even lower-level API as it used to be.
Last updated: Nov 29 2023 at 19:01 UTC