The Coq mailing list

[Ben Horsfall <ben.horsfall AT gmail.com>]

On 14 Jan 2014, at 1:56 pm, Bill Richter 
<richter AT math.northwestern.edu>
 wrote:

> I have bad news: I can not compile coq-8.3pl2, the version needed for 
> Vladimir's Foundations, on either of my two SL machines.  Here's a bug 
> report for the better of the two.

> File "pretyping/pretype_errors.ml", line 48, characters 4-109:
> Error: Unbound constructor Stdpp.Exc_located
> make[1]: *** [pretyping/pretype_errors.cmx] Error 2
> make[1]: Leaving directory `/tmp_mnt/rhome/2/richter/coq-8.3pl2'
> make: *** [world] Error 2

I ran into this problem on Mac OS. See 
https://coq.inria.fr/bugs/show_bug.cgi?id=2728 for an explanation. 
Compilation succeeded for me using ocaml-3.12.1 + camlp5-6.02.3 (which I had 
lying around).


Ben

Attachment: smime.p7s
Description: S/MIME cryptographic signature