coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Syntax of "Parameter"

From: Hugo Herbelin <herbelin AT pauillac.inria.fr>
To: claudia AT consiste.dimap.ufrn.br (Claudia Fernanda Oliveira K Tavares)
Cc: coq-club AT pauillac.inria.fr
Subject: Re: [Coq-Club] Syntax of "Parameter"
Date: Wed, 10 Nov 2004 14:34:10 +0100 (MET)
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

  Hi,

> I've received some examples to test in Coq, but they have some problem. I
> think that is a changing of syntax.

  To re-use your examples, call coqtop with option "-v7" or translate
your files by calling coqc with option "-translate". More about how to
translate in ftp://ftp.inria.fr/INRIA/coq/V8.0pl1/doc/Translator.ps.

  Hugo Herbelin

[Coq-Club] Syntax of "Parameter", Claudia Fernanda Oliveira K Tavares
- Re: [Coq-Club] Syntax of "Parameter", casteran
- Re: [Coq-Club] Syntax of "Parameter", Hugo Herbelin