Stream: MetaCoq

Topic: Gallina quotation


view this post on Zulip Jason Gross (Apr 03 2023 at 03:37):

Btw, if I can get help with / figure out #893, once my current batch of ~14 PRs is merged, I'll have a PR ready implementing quote : Ast.term -> Ast.term (actually, it can quote everything up to the end of Template.Typing, though I'm still trying to work out the universe issues with Template.TypingWf). (And if we want a similar thing for PCUIC, we can probably create a close replica of the current code for PCUIC.)

view this post on Zulip Jason Gross (Apr 05 2023 at 01:30):

The Gallina quotation PR (#894) passes CI and is ready for review! (I am still trying to make the universes consistent with TypingWf, but that can be a separate PR; I expect it will not change the bulk of how things are written. And I might not manage it anytime soon, so it seems better to get the quotation PR in before it bitrots.) This PR is, alas, pretty big (+4623,-16). Happy to add documentation on organization or what's going on or whatever if that's useful.


Last updated: Jul 23 2024 at 20:01 UTC