Stream: Coq users

Topic: ✔ Help with plugins

view this post on Zulip Oliver Flatt (Jul 13 2021 at 18:15):

Hi, I'm trying to build the coq plugin tutorial (coq/doc/plugin_tutorial) and I need some help. tuto0 builds just fine but tuto1 gives me an error:
File "src/simple_declare.ml", line 3, characters 14-29: 3 | let scope = Locality.Global Locality.ImportDefaultBehavior in Error: Unbound constructor Locality.Global

Does anybody know the cause? I'm using OCaml 4.11.2 and coq 8.12.2. Thanks!

view this post on Zulip Gaëtan Gilbert (Jul 13 2021 at 19:34):

you must use the same Coq version as the plugin tutorial

view this post on Zulip Oliver Flatt (Jul 13 2021 at 20:28):

Oh I see, the same version as my clone of the repo. Thanks!

view this post on Zulip Notification Bot (Jul 13 2021 at 20:28):

Oliver Flatt has marked this topic as resolved.

Last updated: Apr 20 2024 at 08:02 UTC