The Coq mailing list

[Yves Bertot <Yves.Bertot AT sophia.inria.fr>]

JAEGER, Eric (SGDN) wrote:
> 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
Well, as Mathieu said, there should not be any reduction happening.  
This should not be the problem...

Yves