The Coq mailing list

[Gabriel Scherer <gabriel.scherer AT gmail.com>]

> 1) What am I doing wrong in this particular example?

Given that your hypothesis is (A = (3,4) /\ (x,y) = A), you apparently
want to destruct over (foo /\ bar) rather than (foo * bar). Changing
your tactic from

match goal with
  | p: ?K * ?V |- _ => ...

to

match goal with
  | p: ?K /\ ?V |- _ => ...

works fine on my machine.

> I don't know emacs. I don't know proof general. Is there any other way to
> debug ltac?

I'm not sure what you mean by "debug Ltac", but regarding coq-modes,
you may consider giving Emacs a try (it is rather easy to use in a
simple way, and I know some long-time vimers use Emacs just for
Proof-General). There is also a fairly young project or providing a
proof-general-like interface for Vim, named "Coquille" (
https://github.com/trefis/coquille ). It's in an early stage of
development, but you may give it a try.

On Sat, May 25, 2013 at 10:19 AM, Math Prover 
<mathprover AT gmail.com>
 wrote:
> There are two separate questions here:
>
> 1) What am I doing wrong in this particular example and
>
> 2) What should I use in general?
>
> ### What am I doing wrong in this example?
>
> I want a tactic that destructs pairs (this is not what I want to do, this is
> my minimal failure case). Yet, when I type in "tac00", I get:
>
> |Error: No matching clauses for match goal
> |       (use "Set Ltac Debug" for more info).
>
>
> ### How do I debug Ltac?
>
> I have used Vim for 10+ years. I have used both CoqIde and Matthieu
> Cartier's http://www.vim.org/scripts/script.php?script_id=4388 .
>
> I don't know emacs. I don't know proof general. Is there any other way to
> debug ltac?
>
> Thanks!