The Coq mailing list

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

Option -rectypes should no longer be needed. You probably have an old
mltop.cmx around and you need to regenerate the dependencies
files. Did you "make clean"?

Hugo Herbelin

On Thu, Dec 20, 2012 at 02:39:51PM +0800, Edward Z. Yang wrote:
> Hey all,
> 
> I'm getting this error when I'm trying to build the latest Coq from Git:
> 
> cd kernel/byterun/ && \
>       "ocamlmklib" -oc coqrun coq_fix_code.o coq_memory.o coq_values.o 
> coq_interp.o
> COQMKTOP -o bin/coqtop
> File "/tmp/coqmain54c3cb.ml", line 1, characters 0-1:
> Error: Unit Coqmain54c3cb imports from Mltop, which uses recursive types.
>        The compilation flag -rectypes is required
> make[1]: *** [bin/coqtop] Error 2
> make[1]: Leaving directory `/srv/code/coq-git'
> make: *** [world] Error 2
> 
> Anyone know what's up?  Should I file a bug?
> 
> Cheers,
> Edward