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!
you must use the same Coq version as the plugin tutorial
Oh I see, the same version as my clone of the repo. Thanks!
Oliver Flatt has marked this topic as resolved.
Last updated: Jan 28 2023 at 06:30 UTC