The Coq mailing list

[Beta Ziliani <beta AT mpi-sws.org>]

Hi all,

I'm having problems with the ML top level: I cannot do anything useful
(not even go back to Coq).

I've set the COQTOP variable pointing to the source files (i.e. the
root Coq directory), and I'm running coqtop.byte. This is the output
after Dropping:

Coq < Drop.
        Objective Caml version 3.11.2

        Camlp5 Parsing version 5.14

#

but if I want to go back to Coq, this is what happens:

# go();;
Error: Unbound value go

It seems like it's not loading any Coq source but I don't see what I'm
doing wrong. Any ideas? I'm using Coq trunk version:

The Coq Proof Assistant, version trunk (December 2011)
compiled on Dec 15 2011 18:28:45 with OCaml 3.11.2


Thanks,
Beta