Is support for generating [Hint Resolve]s something that you anticipate being relatively easy (like for Hint Opaque)? If so I can open an issue :~)
We would like to generate these registrations to ease the burden on new users involved in properly automating constructs/abstractions which they introduce.
Yes, that should be simple as well. Open an issue please, plz.
Thanks for working on all of the issues that Gordon and I have been creating :~) We're having very good results with Elpi so far, and your support has been a big part of that!
OK, now that I'm "done" with https://github.com/LPCIC/coq-elpi/pull/324 I'll try to make a new release with all this little stuff.
@Gordon Stewart do you want me to also finish functors? Or you plan to work on it?
Sorry; I haven't had a chance to finish https://github.com/LPCIC/coq-elpi/pull/332 yet.
What do you think about merging that (just functors, no application, but with the warning fix you mentioned)? Then functor application could perhaps go in a separate MR.
Fine. I just wanted to avoid double work. If you are not working on it, I might. If you do, just tell me.
OK. No, I'm not actively working on it (it turns out I don't need to generate functor applications, then I got sidetracked by other things). For now, I'll fix the warning in https://github.com/LPCIC/coq-elpi/pull/332, then hand the MR over to you.
Last updated: Jun 06 2023 at 22:01 UTC