Is there a documentation/a tutorial that focueses on the tactic aspect (instead of the metaprorgramming aspect) of Ltac2? In particular, I am wondering how/when exactly to use
Control.focus, etc. It seems I can make my tactics almost work with combinations of the two. But tiny changes (e.g. mutating a record field between two calls to
focus, or in the continuation given to
focus) lead to
Tactic failure: Proof search failed. without any backtrace from
Set Ltac2 Backtrace.
My concrete problem is already solved. It was a case of bad error messages combined with a bad programmer. :) I also figured out that the primitives in
Control map pretty much directly to the
Proofview module and the functions in there have some documentation that helped me understand what was going on.
Let me bet you’re not the only one confused, but there’s only so much time :-)
Last updated: Sep 26 2023 at 12:02 UTC