Janno (Oct 29 2020 at 11:44): Janno (Oct 29 2020 at 11:44):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.enter, 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.
Janno (Oct 29 2020 at 14:31):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.
Paolo Giarrusso (Oct 29 2020 at 16:30):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