Checker: don't use monomorphic universes attached to a constant

They are supposed to be included in the module's constraints.

The old behaviour would allow a crafted vo, using
~~~coq
Definition a := Type.
Definition b := Type.

Definition b_in_a : a := b.
Definition a_in_b : b := a.
~~~
with the constraints for b_in_a and a_in_b not included in the module
constraints, then a proof of false may be derived in the usual way.

0 files changed, 0 insertions, 0 deletions