Stream: Coq devs & plugin devs

Topic: Ltac2 Binder.make


view this post on Zulip 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)

view this post on Zulip 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: May 28 2023 at 16:30 UTC