The Coq mailing list

[Tie Cheng <chengtie AT gmail.com>]

Hello all,

I just upgraded the coq under my ubuntu, I compiled the codes in coq-8.3pl1.tar.gz, and the coqide gives the version information as follows:

The Coq Proof Assistant, version 8.3pl1 (décembre 2010)

Architecture win32 running Win32 operating system

Gtk version is 2.18.7

This is the native version (native is the best one for this architecture and OS)

I am trying to run a very simple program which works well under the coq under my Windows 7, this coqide gives the version information:

The Coq Proof Assistant, version 8.3pl1 (February 2011)

Architecture i686 running Unix operating system

Gtk version is 2.22.0

This is the native version (native is the best one for this architecture and OS).

The program which works well under windows looks like:

Require Import Bool Omega ZArith List.

Inductive poly : Type :=

  | Cst : Z -> poly (* Omega makes Z work *)

  | Poly : poly -> nat -> poly -> poly.

Definition p1 : poly := Cst 0. (* 0 *)

Definition p2 : poly := Poly (Cst 0) 1 (Cst 1). (* 0 + X1 * 1 *)

However, when i run it with the new coq under ubuntu, when i "Forward one command", it goes DIRECTLY to the line before the last one. So i got an error "Error: The reference poly was not found in the current environment." That means it does not recognize "poly" just defined above, that means it skipped several lines.

It seems that some .v files work well in both versions of coq, but i really do not see what is wrong with my this piece of code...

Does anyone know what happened?

Many thanks and kindly regards

Tie