Let’s say I have a fancy tactic that solves lemmas of a certain kind: Ltac solveFancy := some_preparation; repeat (first [important_step1 | important_step2]; some_cleanup); solve_basecase. N...

I have a goal that contains a call to some lemma foo within branch of a match. That call uses as one of its arguments a variable R local to the branch: | SomeConstr => fun R => .... (foo a b...

How can I invoke rewrite in ltac to only rewrite one occurrence? I think coq's documentation mentions something about rewrite at but I haven't been able to actually use it in practice and there are...

When implementing a complex tactic in Ltac, there are some Ltac commands or tactic invocation that I expect to fail and where that is expected (e.g. to terminate a repeat, or to cause backtracking)...

I want to make a Ltac tactic in coq which would take either 1 or 3 arguments. I have read about ltac_No_arg in the LibTactics module but if I understood it correctly I would have to invoke my tacti...

In coq, the destruct tactic has a variant accepting an "conjunctive disjunctive introduction pattern" that allows the user to assign names to introduced variables, even when unpacking complex induc...

I am trying to write a rule for hypotheses, formulated with a help of match construction: Goal forall x:nat, (match x with | 1 => 5 | _ => 10 end = 5 -> x = 1)%nat. intros. x : nat H : m...

While trying to create an Ltac definition that loops over a variable-length argument list, I encountered the following unexpected behavior on Coq 8.4pl2. Can anyone explain it to me? Ltac ltac_loo...