Jasper Haag (Feb 01 2022 at 21:10): Jasper Haag (Feb 01 2022 at 21:10):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.
Enrico Tassi (Feb 01 2022 at 21:11):Yes, that should be simple as well. Open an issue please, plz.
Jasper Haag (Feb 01 2022 at 21:16):https://github.com/LPCIC/coq-elpi/issues/337
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!
Enrico Tassi (Feb 01 2022 at 21:33):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?
Gordon Stewart (Feb 01 2022 at 21:46):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.
Enrico Tassi (Feb 01 2022 at 21:48):Fine. I just wanted to avoid double work. If you are not working on it, I might. If you do, just tell me.
Gordon Stewart (Feb 01 2022 at 21:51):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: Oct 13 2024 at 01:02 UTC