The Coq mailing list

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

On Wed, Dec 28, 2011 at 12:00 PM, Hugo Herbelin 
<Hugo.Herbelin AT inria.fr>
 wrote:
> Hi Beta,
>
>
> 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
>

Thanks Hugo, but I forgot to mention something important:

# #use "include";;
Cannot find file include.

It's like if it's not taking COQTOP into account, although it is well set:

$ ls $COQTOP
CHANGES        CREDITS      INSTALL.ide     Makefile         ...