coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] user-defined tactic in some hypothesis

From: frederic.blanqui AT loria.fr
To: coq-club AT pauillac.inria.fr
Subject: Re: [Coq-Club] user-defined tactic in some hypothesis
Date: Thu, 29 May 2008 08:56:41 +0200 (CEST)
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

On Thu, 29 May 2008, Yves Bertot wrote:

In general, I don't believe there is a systematic way to transform a tactic that is supposed to work on the goal into a tactic that is supposed to work on an hypothesis.

in a context h1 .. hn |- G, by seeing the targeted hypothesis hi like a goal in the context h1 .. hi-1 |- hi ?

[Coq-Club] Coq Feature Requests, Michael Day
- [Coq-Club] user-defined tactic in some hypothesis, frederic . blanqui
  - Re: [Coq-Club] user-defined tactic in some hypothesis, Yves Bertot
    - Re: [Coq-Club] user-defined tactic in some hypothesis, frederic . blanqui
  - Re: [Coq-Club] user-defined tactic in some hypothesis, Andrew McCreight
    - Re: [Coq-Club] user-defined tactic in some hypothesis, frederic . blanqui
      - Re: [Coq-Club] user-defined tactic in some hypothesis, Arnaud Spiwack