The Coq mailing list

[Vladimir Voevodsky <vladimir AT ias.edu>]

Bill,

can you try to patch and then compile 8.3pl5 instead and let us know how it 
works?

Thanks!
V.


On Jan 13, 2014, at 10:51 PM, Ben Horsfall 
<ben.horsfall AT gmail.com>
 wrote:

> 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
>