Hi, I'm working on a MetaCoq implementation of the Coq guardedness checker. As part of that, I have changed the MC representation of inductives to incorporate the recargs tree for inductive bodies (what corresponds to
mind_recargs in the OCaml impl).
Of course, that also requires adding that to TemplateCoq's quoting mechanism. I've changed the quoting functions to quote the wf_paths when quoting inductive bodies.
However, I'm having trouble with adding the right references to the Coq term constructors in
src/constr_reification.ml. Since the type
wf_paths is available in
theories/Ast.v under that name, I thought that
let twf_paths = ast "wf_paths" in
src/constr_reification.ml would be the right thing.
But when using this for quoting in Coq, I get
Error: not found in table: metacoq.ast.wf_paths.
So in short, I suppose my assumptions about how the lookup mechanism for the Coq names works are wrong.
Can someone please push me in the right direction? Where do I need to look to find out the right names I need to use in
src/constr_reification.ml to reference my new Coq type?
You probably need the Register command, search the code for other uses to see how it's used
You need to register them in
Thanks a lot, that made it work
Last updated: Dec 07 2023 at 06:38 UTC