Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Question about tactics and conversions

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Question about tactics and conversions


chronological Thread 
  • 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).
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





Archive powered by MhonArc 2.6.16.

Top of Page