The Coq mailing list

["Benjamin C. Pierce" <bcpierce AT cis.upenn.edu>]

Any suggestions from the community on how to make custom entries work better 
here would be greatly appreciated.  We would like to use the new features in 
the next release of Software Foundations (for which the timeline is rather 
tight), but right now we are blocked on several things that appear to be 
either inconveniently rigid in the design or not working as documented.  :-(

Thanks!

    - Benjamin 

> On Sep 22, 2019, at 1:33 PM, Konstantinos Kallas 
> <kallas AT seas.upenn.edu>
>  wrote:
> 
> Hi all,
> 
> We are trying to define the syntax of a simple imperative language using 
> the Custom entries feature but we are encountering some problems. Some of 
> the problems might not be related to custom entries per se, but might be 
> caused by some misuse of the notation feature (due to my lack of 
> understanding of parsing in Coq).
> 
> I have attached a file that contains the definitions, some examples that 
> work as expected, and some examples where the parser gets confused (that 
> are annotated with "Question:" comments).
> 
> It would be great if someone could give us some hints about what could be 
> the problem or how should we go about solving it.
> 
> Thanks,
> Konstantinos

Attachment: ImpCustomEntriesExperiment.v
Description: Binary data