Notation in Universes is incompatible with CertiCoq

[yforster]

Notation "⟦ u ⟧_ v" := (Universe.univ_val v u) (at level 0, format "⟦ u ⟧_ v", v ident) : univ_scope.

in Template.Universes is incompatible with notations in CertiCoq. Maybe we should hide it in a Module?

In CertiCoq, I can't define ⟦ u ⟧ := ... anymore, since now the parser always expect the token ⟧_, even if the new notation is the default interpretation.

[mattam82]

Yes, it should definitively be hidden in a module