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 `template-coq/theories/Constants.v`

indeed

Thanks a lot, that made it work

Last updated: Jul 24 2024 at 12:02 UTC