The Coq mailing list

[Vincent Siles <vincent.siles AT ens-lyon.org>]

Oh right, I didn't thought that the parser would stop at . but it
makes perfect sense.

Thank you
Vincent


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.
>
>  Cheers,
> Georges
>
> -----Original Message-----
> From: Vincent Siles 
>Â [mailto:vincent.siles AT ens-lyon.org]
> Sent: 16 January 2012 10:58
> To: Coq-Club Club
> Subject: [Coq-Club] strange behaviour of Coq / Proof General
>
> I'm running Proof General 4.0 and Coq 8.3 (r14556, last october), and I 
> have a weird behaviour of Coq which is hidden by Proof General.
>
> If I try to compute
> Eval compute (3)./2.
>
> in coqtop, It actually evaluates (to 3) and gives me the message
>
> Toplevel input, characters 20-21:
>> Eval compute in (3)./2.
>>                     ^
> Syntax error: illegal begin of vernac.
>
>
> If I do the same in emacs / pg, I don't have the error message (it is 
> written in the *coq* buffer but there is nothing shown at first), so I this 
> that the answer is 3.
>
> Why is this evaluated to the identity function when no libraries is loaded ?
>
> Best,
> Vincent
>
>