Is there a way to disable backtracking in Ltac match? I trying to debug a tactic where one of the branches fails. So instead of a meaningful error I get "no matching clauses for match".
Ltac foo := match goal with | [..... |- _] => step1; step2; step3; step4 end.
One of the steps fails, but backtracking eats the error message. I wonder if there is a way to debug this.
I think that what you are looking for is called
lazymatch. It is described succintly as a variant of match.
I have a question on cbn and simpl. I try to replace some uses on simpl in VST with cbn cause I have cases where simpl runs forever while cbn returns immediately. One issue is that VST has tactics which take simplification tactics as arguments. Passing simpl or idtac works fine, but passing cbn gives "undefined". Also Print cbn says it is undefined. Init has:
Ltac2 Notation "cbn" s(strategy) cl(opt(clause)) :=
Std.cbn s (default_on_concl cl).
Ltac2 Notation cbn := cbn.
@Théo Zimmermann already explained me that I have to Add Ltac cbn := cbn but it would be nice to understand what these 4 levels of definitions are good for (the core cbn in OCaml, the 2 notations in Init and the Ltac definition needed to pass it as Ltac). Also I wonder if this could be more consistent or if there are some principal restrictions.
Sorry, this was silly - I didn't see that this are Ltac2 Notations. So is there a difference between simpl and cbn visible in the standard library?
Yes, even if you don't load Ltac2,
simpl is an Ltac reference while
cbn is only a
Could you point me to these definitions? I am unable to find them. When I do in a plain session "Locate simpl" it says "Ltac Coq.Init.Notations.simpl"m but the word "simpl" doesn't seem to appear in Init.Notations.
They are defined in the Ltac (ML) plugin. That's why the
Print Ltac command can only show
Ltac simpl := simpl
Last updated: Sep 23 2023 at 08:01 UTC