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

metacoq/common/theories/Environment.v

Lines 372 to 379 in 5672294

	(** See [mutual_inductive_body] from [declarations.ml]. *)
	Record mutual_inductive_body := {
	ind_finite : recursivity_kind;
	ind_npars : nat;
	ind_params : context;
	ind_bodies : list one_inductive_body ;
	ind_universes : universes_decl;
	ind_variance : option (list Universes.Variance.t) }.

So if you want to change one, you have to change both.