The Coq mailing list

[Lionel Elie Mamane <lionel AT mamane.lu>]

In some situations, Ltac tells me:

 User error: No matching clauses for match goal
            (use "Debug On" for more info)

Is this debug mode documented anywhere? Couldn't find it. When I do
"Debug On." and then repeat my command, I get some explanation of the
form:

 ---> cut <----
 The goal has been successfully matched!
 Let us execute the right-hand side part...

 Goal:
 ---> cut <----
 Going to execute:
 apply K_dec with (P := foo)

But then I get a prompt of the form

 TcDebug (1) > 

and I don't know what to type there. Quid?

Thanks in advance for your help,

-- 
Lionel