coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Simplification d'un argument dans une tactique

From: David Nowak <David.Nowak AT lineone.net>
To: David Delahaye <delahaye AT jurancon.inria.fr>
Cc: coq-club AT pauillac.inria.fr
Subject: Simplification d'un argument dans une tactique
Date: Thu, 05 Jul 2001 16:57:22 +0100

Bonsoir David,

Est-il possible de simplifier un argument d'une tactique avant de le
filtrer de mani�re � ce que genre de filtre fonctionne ?

Match ([x:nat]x=x O) With [?1=?2] -> Cut ?1=?2.

Merci,

David.

--
David Nowak
Oxford University Computing Laboratory
tel: +44 1865 283527 home: 248014 fax: 273839
http://web.comlab.ox.ac.uk/oucl/people/david.nowak.html

Filtrage d'un type d�pendant dans une tactique, David Nowak
- Re: Filtrage d'un type d�pendant dans une tactique, David Delahaye
  - Simplification d'un argument dans une tactique, David Nowak
    - Re: Simplification d'un argument dans une tactique, David Delahaye