The Coq mailing list

["Edward Z. Yang" <ezyang AT MIT.EDU>]

Nope, I did a make clean, checked that there were no cmx files in my source
directory, and still am getting build errors.

To be clear, I'm on this commit:

commit 787e409e773d45da6d149fbcdf9657b0be4a5529
Author: pboutill <pboutill@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date:   Wed Dec 19 22:34:35 2012 +0000

    Reductionops reduction machine can refold constant
    
    git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16107 
85f007b7-540e-0410-9357-904b9bb8a0f7

Cheers,
Edward

Excerpts from Hugo Herbelin's message of Thu Dec 20 15:22:31 +0800 2012:
> 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