diff options
Diffstat (limited to 'engine/universes.ml')
| -rw-r--r-- | engine/universes.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/engine/universes.ml b/engine/universes.ml index 70601987c..ee9668433 100644 --- a/engine/universes.ml +++ b/engine/universes.ml @@ -17,7 +17,7 @@ type universe_binders = UnivNames.universe_binders type univ_name_list = UnivNames.univ_name_list let pr_with_global_universes = UnivNames.pr_with_global_universes -let reference_of_level = UnivNames.reference_of_level +let reference_of_level = UnivNames.qualid_of_level let add_global_universe = UnivNames.add_global_universe |