coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Problem with tactics...

From: Pierre Corbineau <Pierre.Corbineau AT lri.fr>
To: Romain Janvier <Romain.Janvier AT imag.fr>
Cc: coq-club AT pauillac.inria.fr
Subject: Re: [Coq-Club] Problem with tactics...
Date: Tue, 25 Feb 2003 17:04:55 +0100
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

On Tue, Feb 25, 2003 at 04:38:39PM +0100, Romain Janvier wrote:
> I want to write something like that in a tactic:
>
> Tactic Definition tac:=
> Match Context With
> ...
> |[id: (EX ?1| ?2)|-?3] -> Induction id
> ...

Use the pattern [id: (ex ? ? ?)|-?] instead.

--
Pierre Corbineau         |
Pierre.Corbineau AT lri.fr
LRI                      | Tel: 01 69 15 64 85
Bat. 490-Univ. Paris-Sud | Bureau 145b
91405 Orsay Cedex        | http://clipper.ens.fr:8080/home/corbinea/index.html

[Coq-Club] Problem with tactics..., Romain Janvier
- Re: [Coq-Club] Problem with tactics..., Benjamin GREGOIRE
- Re: [Coq-Club] Problem with tactics..., Pierre Corbineau
  - [Coq-Club] Turning off special pretty-printing, Robert R. Schneck
    - Re: [Coq-Club] Turning off special pretty-printing, Hugo Herbelin