diff options
Diffstat (limited to 'engine/universes.ml')
| -rw-r--r-- | engine/universes.ml | 5 |
1 files changed, 0 insertions, 5 deletions
diff --git a/engine/universes.ml b/engine/universes.ml index ee9668433c..5d0157b2db 100644 --- a/engine/universes.ml +++ b/engine/universes.ml @@ -19,14 +19,9 @@ type univ_name_list = UnivNames.univ_name_list let pr_with_global_universes = UnivNames.pr_with_global_universes let reference_of_level = UnivNames.qualid_of_level -let add_global_universe = UnivNames.add_global_universe - -let is_polymorphic = UnivNames.is_polymorphic - let empty_binders = UnivNames.empty_binders let register_universe_binders = UnivNames.register_universe_binders -let universe_binders_of_global = UnivNames.universe_binders_of_global let universe_binders_with_opt_names = UnivNames.universe_binders_with_opt_names |