coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Problem with defining a new vernacular command

From: Fritjof <fritjof AT uni-bremen.de>
To: coq-club AT inria.fr
Subject: [Coq-Club] Problem with defining a new vernacular command
Date: Thu, 3 May 2018 09:33:00 +0200
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=fritjof AT uni-bremen.de; spf=Pass smtp.mailfrom=fritjof AT uni-bremen.de; spf=None smtp.helo=postmaster AT smtp.uni-bremen.de
Ironport-phdr: 9a23:CerPLxUPNNS7a8Cb7kzIIoPZH7jV8LGtZVwlr6E/grcLSJyIuqrYYxSCt8tkgFKBZ4jH8fUM07OQ7/i7HzRYqb+681k6OKRWUBEEjchE1ycBO+WiTXPBEfjxciYhF95DXlI2t1uyMExSBdqsLwaK+i764jEdAAjwOhRoLerpBIHSk9631+ev8JHPfglEnjWwba98IRmssQndqtQdjJd/JKo21hbHuGZDdf5MxWNvK1KTnhL86dm18ZV+7SleuO8v+tBZX6nicKs2UbJXDDI9M2Ao/8LrrgXMTRGO5nQHTGoblAdDDhXf4xH7WpfxtTb6tvZ41SKHM8D6Uaw4VDK/5KptVRTmijoINyQh/W/ZisJ+kr9VrhGuqBNj3oHbbpqYNOZicq7HYd8WWXBMU8RXWidcAo28dYwPD+8ZMOhYtYn9pkcOrRm5BQmiGejizTFIhmX33a0m0eQhFg/G0Rc9H9IIsXTYtc76NL0MXuCw0qbIyy/PYO5I1jrk7oXDbxMvoemUUL5tf8fcxlMjGx7ZglmOs4DoPy+Z2v4Qv2SH9+ZsSOyihmE9pw1svjSj2N0ghpfUio8W0FzI6yV0zJszKNalUkB0e8SkH4FVtyyCN4t5XMciQ2ZwtSYhz70GpYa7cDIXyJQhxh7TcueIc5KW7RLmSumRJy10i297d76nhhay91avyvHkW8Wp3ltHoTBJnsTQunwTzRDe6tSLRuFg8ku9wTqP0hrc6uBAIUA6j6rbLJshz6Y+lpoJsETDAi32mEL4jKKNa0Uk/Omo5/38bbX8uJCcMpF7igfkPqszhMOzGf44PRQWX2iH5eS806Xu8lH+QLVTl/E5jq3ZsI3BKskAva64AwpV0p455BqlDjem1s4YnXgdI15fdhKHlduhB1abK/fhSPy7nl6EkTFxxvmAMKeyLI/KKy3tirb9f7FzoxpS0gsvz9dRz49SC/QLOv/2V0m3uNGOXUxxCBC93+uyUIY17YgZQ2/aWvbIYpOXikeB46cUG8fJYYYUvDjnLP18uqzzi358k0UQeKSvm5caOinhQqZWZn6BaH+pue8vVH8Qt1NjHvHsiRiISzNWanD0U69uvmhmWrLjNp/KQ8WWuJLE3Cq/GccONHtDFkjKDHHpMo+eVvIBbmSeL505nw==

Hi,

I have a problem defining a new vernacular since Coq 8.8.0 - I guess.
I think in a previous version this worked.

g_foo.ml4:
DECLARE PLUGIN "foo_plugin"

VERNAC COMMAND EXTEND FooBar CLASSIFIED AS QUERY
| [ "Foo" "Bar" ] -> [ Foo.bar () ]
END

Coqtop:
Coq < Declare ML Module "foo_plugin".
[Loading ML file foo_plugin.cmxs ... done]

Coq < Foo Bar.
Toplevel input, characters 0-3:
> Foo Bar.
> ^^^
Error: Syntax error: illegal begin of vernac.

$ make

COQDEP VFILES
COQDEP foo_plugin.mllib
CAMLDEP foo.ml
CAMLDEP -pp g_foo.ml4
CAMLOPT -a -o foo_plugin.cmxa
CAMLOPT -shared -o foo_plugin.cmxs

make(1) runs with no errors.

Does anyone have a hint, why "Foo Bar." does not work, even if I defined it
and make(1)
processes the grammar file?

Best,
--f.

[Coq-Club] Problem with defining a new vernacular command, Fritjof, 05/03/2018
- Re: [Coq-Club] Problem with defining a new vernacular command, Gaëtan Gilbert, 05/03/2018
  - Re: [Coq-Club] Problem with defining a new vernacular command, Fritjof, 05/03/2018
    - Re: [Coq-Club] Problem with defining a new vernacular command, Gaëtan Gilbert, 05/03/2018
      - Re: [Coq-Club] Problem with defining a new vernacular command, Emilio Jesús Gallego Arias, 05/03/2018
      - Re: [Coq-Club] Problem with defining a new vernacular command, Fritjof Bornebusch, 05/04/2018