Universe checking state gets confused when locally changed in module

[SkySkimmer]

Universes u v.

Constraint u < v.

(* also happens with Module Type *)
Module Off.
  Local Unset Universe Checking.
End Off.
Test Universe Checking. (* on *)

From Stdlib Require Import Hurkens.

Lemma bad : False.
Proof.
  eapply TypeNeqSmallType.paradox; reflexivity.
Defined.

Print Assumptions bad.
(* closed under the global context *)

This happens because ugraph contains a copy of the flag which gets out of sync when closing the module.