coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Syntax for morphisms in Coq 8.2?

From: "Andrew McCreight" <continuation AT gmail.com>
Cc: coq-club AT pauillac.inria.fr
Subject: Re: [Coq-Club] Syntax for morphisms in Coq 8.2?
Date: Wed, 1 Oct 2008 07:30:08 -0700
Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=message-id:date:from:subject:cc:in-reply-to:mime-version :content-type:references; b=RLLK24yr2UYPOVHhtREydL3d4ybSj3sDLCuDbeDjMIIDyYnuwESi0drIcyznA1rW5o TCcnuo6dei9hGBgB7R/EEY3LJZV2bYi+FSEIWYX9TpPU6m+Q3Un43rbBl0Ape6Rf55mY QRaZDzWwMhYiUaYw58NjevJcRar6MN0NBJhiA=
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

Yes, the syntax has changed. You can look in the manual for the new version [1] for the new syntax. I don't recall it offhand. There are some other minor incompatibilities for setoid rewriting which you may have to deal with.

[1] http://coq.inria.fr/V8.2beta4/doc/refman/html/

On Tue, Sep 30, 2008 at 9:16 AM, Edsko de Vries <devriese AT cs.tcd.ie> wrote:

Hi,

Did the syntax for morphisms change in Coq 8.2? I have

Add Morphism or
with signature equiv ==> equiv ==> equiv
as or_morphism.

in my development, which works fine with 8.1 but gives this error in 8.2:

Error while reading ./BooleanAlgebraM.v:File "./BooleanAlgebraM.v", line 65, characters 23-26:
Syntax error: 'as' expected after [constr:lconstr] (in [vernac:command])

Thanks,

Edsko

--------------------------------------------------------
Bug reports: http://logical.futurs.inria.fr/coq-bugs
Archives: http://pauillac.inria.fr/pipermail/coq-club
http://pauillac.inria.fr/bin/wilma/coq-club
Info: http://pauillac.inria.fr/mailman/listinfo/coq-club

Re: [Coq-Club] Syntax for morphisms in Coq 8.2?, Andrew McCreight