Add trans_one_inductive_entry
#789
Conversation
|
Ah, I see. It's just that PCUIC was not updated to use a |
To allow `mutual_inductive_entry` to depend on `context`
JasonGross
force-pushed
the
trans_one_inductive_entry
branch
from
e4f316e to
c9f5878
Compare
@mattam82 Done |
pcuic/theories/PCUICToTemplate.v
Outdated
| mind_entry_variance := None (* Should something go here??? *); | ||
| mind_entry_template := false |}. |
There was a problem hiding this comment.
Is this correct? Is PCUIC incapable of doing template-universes, and template-coq incapable of storing variance information?
There was a problem hiding this comment.
I think both should have both fields. But check in quoter.ml for what a particular version of Coq supports, it changes in recent versions.
There was a problem hiding this comment.
Can we make that update in another PR, and merge this one now?
There was a problem hiding this comment.
Actually, it looks like it's just PCUIC that supports neither variance nor template polymorphism.
JasonGross
force-pushed
the
trans_one_inductive_entry
branch
from
a6d2fcb to
496e55c
Compare
|
ping @mattam82 |
|
I’ll have to check, probably this afternoon |
|
ping @mattam82 can this be merged? |
|
Yes, sorry for the delay |
The updated version of MetaCoq#789 managed to define `trans_mutual_inductive_entry`
The updated version of MetaCoq#789 managed to define `trans_mutual_inductive_entry`
Also add a comment with a partial
trans_mutual_inductive_entry. It seems not possible to write this method yet? (I could also drop the commit that adds this partially, if that's preferred.) This is towards #776