Improve Quoting to also quote uniform parameters

[thomas-lamiaux]

From what I understand, uniform and non-uniform parameters are distinguished in the kernel but not in MetaCoq because it does not matter for typing. However, it matters for meta-programming so:

1. quoting should split the context of parameters in uniform and non-uniform one
2. adapt the functions between Template and PCUIC accordingly
   • Template -> PCUIC is trivial, it is just merging back
   • For PCUIC -> template, one will need a function to compute uniform parameters back
     I have one but it relies on my interface, though it should be easily adaptable as it's just reading
     It suffices to replace the state interface by a shift to keep track of the scope

[MevenBertrand]

Alternative approach: make the difference also in PCUIC, and redefine the current field accessors to functions which do the merging (or keep them as fields + proofs that they correspond to the right thing, like we do with the number of parameters). Hopefully we can keep a mostly unchanged interface for the rest of PCUIC, but keeping that information around seems more future-proof: we don't know where/when we'll need that distinction in PCUIC, but I am sure it will happen (honestly, I am surprised it does not already appears in environment typing somehow).

[thomas-lamiaux]

It seems that definitions of inductive types are actually shared between both in Template and PCUIC https://github.com/MetaCoq/metacoq/blob/5672294a99a0275ce8d4e10ded692c3cc92a163e/common/theories/Environment.v#L372-L379
So if you want to change one, you have to change both.