The Coq mailing list

[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