The Coq mailing list

[Pierre Courtieu <Pierre.Courtieu AT cnam.fr>]

2012/1/16 Georges Gonthier 
<gonthier AT microsoft.com>:
>  Because the (ssreflect) library defines the composite symbol ./2. Without 
> that definition Coq parses Eval compute in (3). then sees a lone / 2 whence 
> the syntax error.  The PG segmentation sends the entire fragment in one 
> piece to Coq, expecting a single answer. I guess Coq could follow the same 
> policy and only recognize . + whitespace as the end-of-command marker, 
> though this might  not suit users that string many commands on the same 
> line.

Up to bugs :), pg recognizes only .+spaces as the end of command (and
also the new bullets since very recent dev releases). In pg4.1 and pg
dev release (the latter recommended for coq-8.4beta) I cannot
reproduce this behavior. Hopefully this is an already fixed bug :).
Please let me know if you still have the bug.

Best regards,
Pierre