diff options
Diffstat (limited to 'engine/universes.ml')
| -rw-r--r-- | engine/universes.ml | 8 |
1 files changed, 5 insertions, 3 deletions
diff --git a/engine/universes.ml b/engine/universes.ml index 6c1b64d74..459c53002 100644 --- a/engine/universes.ml +++ b/engine/universes.ml @@ -21,14 +21,16 @@ let pr_with_global_universes l = (** Local universe names of polymorphic references *) -type universe_binders = (Id.t * Univ.Level.t) list +type universe_binders = Univ.Level.t Names.Id.Map.t + +let empty_binders = Id.Map.empty let universe_binders_table = Summary.ref Refmap.empty ~name:"universe binders" -let universe_binders_of_global ref = +let universe_binders_of_global ref : universe_binders = try let l = Refmap.find ref !universe_binders_table in l - with Not_found -> [] + with Not_found -> Names.Id.Map.empty let register_universe_binders ref l = universe_binders_table := Refmap.add ref l !universe_binders_table |