The Coq mailing list

[Math Prover <mathprover AT gmail.com>]

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!

Attachment: fail.v
Description: Binary data