coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] tactics for Z

From: Evgeny Makarov <emakarov AT gmail.com>
To: coq-club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] tactics for Z
Date: Wed, 15 Jun 2011 18:21:29 +0200
Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:in-reply-to:references:date:message-id:subject:from:to :content-type; b=k+1Y1SzAYTY3SvbCtBWtlDD+8OdIYgu3BnqyG6VXgZWghUGtHrDFpr3pYoTMOWoqOq dkRn2YHuqo/kkSfpSHhomks4IlCcfqzxe1shFdvdivmNuLytjrvD/MZm49PbzuJQX/yi 9m0qsI9HY0VrMQo2Um51VvkuBdeLTPTQWB/UY=

> Does nlia reply on any external tools? I think it is not included in
> the 8.3 release. Where can I access the tactic?

It is available in the latest Coq trunk version. You can check it out
using SVN. See https://gforge.inria.fr/scm/?group_id=269 and add
/trunk to the end of the URL.

Evgeny

[Coq-Club] tactics for Z, Jianzhou Zhao
- Re: [Coq-Club] tactics for Z, Fr�d�ric Besson
  - Re: [Coq-Club] tactics for Z, Jianzhou Zhao
    - Re: [Coq-Club] tactics for Z, Evgeny Makarov