The Coq mailing list

["JAEGER, Eric (SGDN)" <eric.jaeger AT sgdn.gouv.fr>]

Thanks for your answers... It seems that I'm looking for non existing 
features of Ltac (for now).
I cannot use [Debug On] because I'm working with CoqIde (Windows version, 
that does not help either ;-) ), but your comment on typechecking is 
probably a solution to my problem.

Indeed, may be I should make explicit coercions in my tactic : f(COER t) 
instead of f(t). If the pattern matching does not typecheck it may not be 
fully aware of coercions (coercions being, if I understood correctly, 
introduced as required to typecheck)... and may try to reduce expressions to 
match, and that is probably the source of my difficulty.

   Regards, Eric

----- Original Message ----- 
From: "Matthieu Sozeau" <Matthieu.Sozeau AT lri.fr>
To: "JAEGER, Eric (SGDN)" 
<eric.jaeger AT sgdn.gouv.fr>
Cc: 
<coq-club AT pauillac.inria.fr>
Sent: Monday, February 02, 2009 10:52 PM
Subject: Re: [Coq-Club] Question about tactics and conversions

I don't think [match goal] involves any conversion but it does not
typecheck patterns either.
You may want to use the [Debug On] command to investigate the bug
further. After this command,
you have to switch to the *coq* buffer (in ProofGeneral, don't know
about coqide) to enter the
debug mode of Ltac. You have to reissue a [Debug Off] command to get
out of it, it has a
non-undoable side-effect.

Hope this helps,
-- Matthieu