The Coq mailing list

[Eddy Westbrook <westbrook AT kestrel.edu>]

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