The Coq mailing list

[Zoe Paraskevopoulou <zoe.paraskevopoulou AT gmail.com>]

Yes, that’s exactly what I did and I found that the import that was missing is Pcoq.Prim! In particular, int() didn’t work, but natural() did work for me and it’s better for my purpose. After looking at Pcoq source code I found that integer() works too.

Thank you all, 

Zoe

On Jan 31, 2020, at 1:21 PM, Talia Ringer <tringer AT cs.washington.edu> wrote:

In that case, if you suspect it's an import, perhaps try copying the imports from the 8.9 version of the file you linked to: https://github.com/coq/coq/blob/v8.9/plugins/ltac/g_ltac.ml4

Perhaps something moved between 8.9 and 8.10? Just a guess, again. For example, the old file has:

open Vernac_classifier

while the new file does not.

On Fri, Jan 31, 2020 at 10:08 AM Zoe Paraskevopoulou <zoe.paraskevopoulou AT gmail.com> wrote:

On Jan 31, 2020, at 12:55 PM, Zoe Paraskevopoulou <zoe.paraskevopoulou AT gmail.com> wrote:

Ah, that’s an interesting observation. My file is an .ml4 file (which seems deprecated for this purpose, but I never knew until now) and the syntax is exactly the syntax that I use in the file (in fact the {} syntax gives me a syntax error in .ml4). But I’ll try to change it to .mlg and see if that works. 

My file is an .ml4 file (which seems deprecated for this purpose, but I never knew until now) and the syntax is exactly the syntax that I use in the file (in fact the {} syntax gives me a syntax error in .ml4).

Actually, it seems that for the version of Coq that we’re using (8.9.1) there’s support for .ml4 files only.