aboutsummaryrefslogtreecommitdiffhomepage
path: root/engine/univNames.ml
diff options
context:
space:
mode:
Diffstat (limited to 'engine/univNames.ml')
-rw-r--r--engine/univNames.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/engine/univNames.ml b/engine/univNames.ml
index 6e59a7c9e..6ffb4bcf0 100644
--- a/engine/univNames.ml
+++ b/engine/univNames.ml
@@ -89,7 +89,7 @@ let register_universe_binders ref ubinders =
if not (Id.Map.is_empty ubinders)
then Lib.add_anonymous_leaf (ubinder_obj (ref,ubinders))
-type univ_name_list = Misctypes.lname list
+type univ_name_list = Names.lname list
let universe_binders_with_opt_names ref levels = function
| None -> universe_binders_of_global ref