coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Simple question about tactic notation

From: Edsko de Vries <devriese AT cs.tcd.ie>
To: Thomas Braibant <thomas.braibant AT gmail.com>
Cc: coq-club AT pauillac.inria.fr, Damien Pous <Damien.Pous AT inria.fr>
Subject: Re: [Coq-Club] Simple question about tactic notation
Date: Sun, 15 Mar 2009 17:05:17 +0000
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

On Sun, Mar 15, 2009 at 05:43:25PM +0100, Thomas Braibant wrote:
> Maybe I am wrong but it seems to be related to a bug we encountered,
> where the n in induction n in your tactic is not linked to the
> parameter integer(n) but to a "n" potentially appearing in the context
> of your goal (and here, I expect you do not have such n in your
> context).
>
> If you write set (n:=1); my_induction 1664. then your tactic works,
> isn't it ?

Yes, indeed. Weird :)

Edsko

[Coq-Club] Simple question about tactic notation, Edsko de Vries
- Re: [Coq-Club] Simple question about tactic notation, Thomas Braibant
  - Re: [Coq-Club] Simple question about tactic notation, Samuel E. Moelius III
    - Re: [Coq-Club] Simple question about tactic notation, Edsko de Vries
      - Re: [Coq-Club] Simple question about tactic notation, Samuel E. Moelius III
        
        Re: [Coq-Club] Simple question about tactic notation, Samuel E. Moelius III
        
        Re: [Coq-Club] Simple question about tactic notation, Edsko de Vries
  - Re: [Coq-Club] Simple question about tactic notation, Edsko de Vries
    - Re: [Coq-Club] Simple question about tactic notation, Edsko de Vries
- Re: [Coq-Club] Simple question about tactic notation, Hugo Herbelin