The Coq mailing list

[Hugo Herbelin <Hugo.Herbelin AT inria.fr>]

Hi Beta,

> 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

Function "go()" is provided in the file "include" from the directory
dev of the source archive. So you'd better do that first

  #use"include";;

Alternatively, you can have this be done automatically by adding a
file .ocamlinit in your home directory with the following content
(trick shown to me by Pierre Letouzey):

  if Filename.basename Sys.argv.(0) = "coqtop.byte"
  then ignore (Toploop.use_silently Format.std_formatter "include")

See file dev/doc/debugging.txt from the source archive for more
information on using the ocaml toplevel.

Hugo