diff options
Diffstat (limited to 'engine/uState.ml')
-rw-r--r-- | engine/uState.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/engine/uState.ml b/engine/uState.ml index df50bae86..ffb54d441 100644 --- a/engine/uState.ml +++ b/engine/uState.ml @@ -24,7 +24,7 @@ module UPairSet = Universes.UPairSet (* 2nd part used to check consistency on the fly. *) type t = - { uctx_names : Universes.universe_binders * uinfo Univ.LMap.t; + { uctx_names : UnivNames.universe_binders * uinfo Univ.LMap.t; uctx_local : Univ.ContextSet.t; (** The local context of variables *) uctx_seff_univs : Univ.LSet.t; (** Local universes used through private constants *) uctx_univ_variables : Universes.universe_opt_subst; @@ -298,7 +298,7 @@ let reference_of_level uctx = fun l -> try CAst.make @@ Libnames.Ident (Option.get (Univ.LMap.find l map_rev).uname) with Not_found | Option.IsNone -> - Universes.reference_of_level l + UnivNames.reference_of_level l let pr_uctx_level uctx l = Libnames.pr_reference (reference_of_level uctx l) |