coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Marko Malikovi� <marko AT ffri.hr>
- To: devriese AT cs.tcd.ie
- Cc: coq-club AT pauillac.inria.fr
- Subject: Re: [Coq-Club] Intro in Ltac - correction
- Date: Thu, 6 Dec 2007 23:44:18 +0100 (CET)
- Importance: Normal
- List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>
Of sure, this is a nonsense:
> Furthermore, even this work:
>
> Ltac test :=
> try (intro H1;idtac).
> Goal 2+3=5 -> 5=5.
> test.
because we did not try to use H1 (what is impossible because it's not
introduced in context).
Marko
- [Coq-Club] Intro in Ltac, Marko Malikoviæ
- Re: [Coq-Club] Intro in Ltac,
Edsko de Vries
- Re: [Coq-Club] Intro in Ltac,
Marko Malikoviæ
- Re: [Coq-Club] Intro in Ltac - correction, Marko Malikoviæ
- Re: [Coq-Club] Intro in Ltac,
Edsko de Vries
- Re: [Coq-Club] Intro in Ltac, Marko Malikoviæ
- Re: [Coq-Club] Intro in Ltac,
Marko Malikoviæ
- Re: [Coq-Club] Intro in Ltac,
Sean Wilson
- Re: [Coq-Club] Intro in Ltac, Marko Malikoviæ
- Re: [Coq-Club] Intro in Ltac,
Edsko de Vries
Archive powered by MhonArc 2.6.16.