coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Yves Bertot <Yves.Bertot AT sophia.inria.fr>
- To: "JAEGER, Eric (SGDN)" <eric.jaeger AT sgdn.gouv.fr>
- Cc: Matthieu Sozeau <Matthieu.Sozeau AT lri.fr>, coq-club AT pauillac.inria.fr
- Subject: Re: [Coq-Club] Question about tactics and conversions
- Date: Tue, 03 Feb 2009 10:18:53 +0100
- List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>
JAEGER, Eric (SGDN) wrote:
Thanks for your answers... It seems that I'm looking for non existing features of Ltac (for now).Well, as Mathieu said, there should not be any reduction happening. This should not be the problem...
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
Yves
- [Coq-Club] Question about tactics and conversions, JAEGER, Eric (SGDN)
- Re: [Coq-Club] Question about tactics and conversions, Yves Bertot
- Re: [Coq-Club] Question about tactics and conversions,
Matthieu Sozeau
- Re: [Coq-Club] Question about tactics and conversions,
JAEGER, Eric (SGDN)
- Re: [Coq-Club] Question about tactics and conversions, Yves Bertot
- Re: [Coq-Club] Question about tactics and conversions,
JAEGER, Eric (SGDN)
- Re: [Coq-Club] Question about tactics and conversions, Matthieu Sozeau
- Re: [Coq-Club] Question about tactics and conversions,
JAEGER, Eric (SGDN)
- Re: [Coq-Club] Question about tactics and conversions, Yves Bertot
- Re: [Coq-Club] Question about tactics and conversions,
JAEGER, Eric (SGDN)
Archive powered by MhonArc 2.6.16.