Trouble adding a new definition to the environment in 8.9.1

Developing plugins
1

I am trying to write a simple plugin that parses a text file and then adds a new term based on the data present in that file. I am following the tutorials present here and I think I can handle setting up the basic plugin scaffolding, the parsing (of course this is just an OCaml task), as well as the creation of the term. What I haven’t been able to figure out is the correct code for adding the term to the environment. I tried using this code snippet (and it’s also worth mentioning that in each of these tutorials I had to change the .mlg file back to an .ml4 file, but this mostly involved changing some curly brackets to square brackets) but I get an error saying that DeclareDef.prepare_definition is not defined. Am I doing something wrong here? (FWIW I am using Coq 8.9.1 installed with Opam)

2

Plugins are highly sensitive to the Coq version, since you looked at the
plugin tutorial for Coq master it’s expected that it doesn’t work with 8.9.
The plugin tutorial for 8.9 is at
https://github.com/ybertot/plugin_tutorials/tree/coq-8.9 (note the
branch) (the tutorial moved from its own repository to Coq’s between 8.9
and 8.10)

Gaëtan Gilbert

3

Thank you for pointing me in the right direction Gaëtan. As a follow-up question, the term I am constructing has type Constr.constr while the packed_declare_definition function from tuto1 expects an argument of type Constrexpr.constr_expr. What is the standard way to convert between these two (or should I not be building a value of type Constr.constr)?

4

try looking at how that function is implemented

Gaëtan Gilbert