The Coq mailing list

[Edsko de Vries <devriese AT cs.tcd.ie>]

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