A unique execution path for the treatement of universes in declare.ml

[herbelin]

Rendered here.

[ejgallego]

Thanks for the CEP @herbelin , I didn't check it deeply but it seems to me that things are going on the right direction.

From my own use cases, the most important bit is to get the most uniformity possible in the case that an opaque proof is present or not.