The Coq mailing list

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

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