diff options
Diffstat (limited to 'engine/univNames.ml')
| -rw-r--r-- | engine/univNames.ml | 15 |
1 files changed, 0 insertions, 15 deletions
diff --git a/engine/univNames.ml b/engine/univNames.ml index 9e4c6e47fc..70cdd3a2db 100644 --- a/engine/univNames.ml +++ b/engine/univNames.ml @@ -11,7 +11,6 @@ open Util open Names open Univ -open Nametab let qualid_of_level l = @@ -31,20 +30,6 @@ let pr_with_global_universes l = Libnames.pr_qualid (qualid_of_level l) (** Global universe information outside the kernel, to handle polymorphic universe names in sections that have to be discharged. *) -let universe_map = (Summary.ref UnivIdMap.empty ~name:"global universe info" : bool Nametab.UnivIdMap.t ref) - -let add_global_universe u p = - match Level.name u with - | Some n -> universe_map := Nametab.UnivIdMap.add n p !universe_map - | None -> () - -let is_polymorphic l = - match Level.name l with - | Some n -> - (try Nametab.UnivIdMap.find n !universe_map - with Not_found -> false) - | None -> false - (** Local universe names of polymorphic references *) type universe_binders = Univ.Level.t Names.Id.Map.t |