The Coq mailing list

[Mandy Martino <tesleft AT hotmail.com>]

Hi  John,

in ubuntu 12 virtual machine using ocqml 3.12.1 but install coq 8.0 got error 
as stated  before.

in ubuntu 14, have 8.4pl6 , have error , so i change to ubuntu 12 machine , 
then have installation error for coq 8.0.
martin@ubuntu:~$ ocaml -version
The OCaml toplevel, version 4.01.0
martin@ubuntu:~$ coqc -version
coqc: -version: no such file or directory
martin@ubuntu:~$ coqc --version
The Coq Proof Assistant, version 8.4pl6 (December 2015)
compiled on Dec 18 2015 23:12:11 with OCaml 4.01.0
martin@ubuntu:~$ 

Error: In environment
x : Z
y : Z
The term "x" has type "Z" while it is expected to have type 
"nat".

is_empty_correct < is_empty_correct < Toplevel input, characters 13-25:
> generalize (compare_spec x z); destruct (compare x z).
>             ^^^^^^^^^^^^
Error: The reference compare_spec was not found in the current environment.

is_empty_correct < 


Regards,

Martin 

________________________________________
寄件者: John Wiegley 
<jwiegley AT gmail.com>
 代表 John Wiegley 
<johnw AT newartisans.com>
寄件日期: 2016年1月24日 3:58
收件者: Mandy Martino
副本: 
coq-club AT inria.fr
主旨: Re: [Coq-Club] how to run this program to verify a simple function?

>>>>> Mandy Martino 
>>>>> <tesleft AT hotmail.com>
>>>>>  writes:

> i have already been using 3.12.1, why still have error?

I'm not sure, but 3.12 and Coq 8.0 are very old versions. Is there any way to
upgrade to OCaml 4 and Coq 8.4pl6? Then I could try your code here, if it is
available online anywhere.

--
John Wiegley                  GPG fingerprint = 4710 CF98 AF9B 327B B80F
http://newartisans.com                          60E1 46C4 BD1A 7AC1 4BA2