diff options
Diffstat (limited to 'library/universes.ml')
| -rw-r--r-- | library/universes.ml | 19 |
1 files changed, 18 insertions, 1 deletions
diff --git a/library/universes.ml b/library/universes.ml index fe5730e95..504a682fc 100644 --- a/library/universes.ml +++ b/library/universes.ml @@ -12,11 +12,14 @@ open Names open Term open Environ open Univ +open Globnames +(** Global universe names *) type universe_names = Univ.universe_level Idmap.t * Id.t Univ.LMap.t -let global_universes = Summary.ref ~name:"Global universe names" +let global_universes = + Summary.ref ~name:"Global universe names" ((Idmap.empty, Univ.LMap.empty) : universe_names) let global_universe_names () = !global_universes @@ -26,6 +29,20 @@ let pr_with_global_universes l = try Nameops.pr_id (LMap.find l (snd !global_universes)) with Not_found -> Level.pr l +(** Local universe names of polymorphic references *) + +type universe_binders = (Id.t * Univ.universe_level) list + +let universe_binders_table = Summary.ref Refmap.empty ~name:"universe binders" + +let universe_binders_of_global ref = + try + let l = Refmap.find ref !universe_binders_table in l + with Not_found -> [] + +let register_universe_binders ref l = + universe_binders_table := Refmap.add ref l !universe_binders_table + (* To disallow minimization to Set *) let set_minimization = ref true |