Hi. I need to solve canonical structure instanciation using coq-elpi. But for this, I need a "hook" in Coq similar to what has been done for coercions. However, I have no idea how I should go about it. Could someone help me doing that?

We can look into it tomorrow. As of today coq does not provide such a hook.

Last updated: Oct 13 2024 at 01:02 UTC