Skip to Content.
Sympa Menu

coq-club - [Coq-Club] Parsing top-level Gallina commands in a plugin

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Parsing top-level Gallina commands in a plugin


Chronological Thread 
  • From: Eddy Westbrook <westbrook AT kestrel.edu>
  • To: coq-club AT inria.fr
  • Subject: [Coq-Club] Parsing top-level Gallina commands in a plugin
  • Date: Thu, 12 Feb 2015 14:22:39 -0800

Hi,

If I am writing a VERNAC ARGUMENT EXTEND to parse my own data-type, is there
a way to have it call out to the parser for top-level Gallina commands? I
would like to use the “gallina” syntactic class, though I would be ok with
“vernac”, “gallina_ext", etc. Specifically, I would like to parse the
“Variable”, “Axiom”, “Definition”, and maybe the “Fixpoint” Gallina commands,
without having to write new versions of those parsing rules myself.

Is this possible? I am using the latest 8.5 beta release.

Thanks,
-Eddy

  • [Coq-Club] Parsing top-level Gallina commands in a plugin, Eddy Westbrook, 02/12/2015

Archive powered by MHonArc 2.6.18.

Top of Page