Reserve "sort_expr" for uninterned universes

1 files changed, 3 insertions, 3 deletions

diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml
index f42c754ef5..d631be18b8 100644
--- a/pretyping/glob_ops.ml
+++ b/pretyping/glob_ops.ml
@@ -60,19 +60,19 @@ let glob_sort_family = let open Sorts in function
   | UNamed [GSet,0] -> InSet
   | _ -> raise ComplexSort
 
-let glob_sort_expr_eq f u1 u2 =
+let glob_sort_gen_eq f u1 u2 =
  match u1, u2 with
   | UAnonymous {rigid=r1}, UAnonymous {rigid=r2} -> r1 = r2
   | UNamed l1, UNamed l2 -> f l1 l2
   | (UNamed _ | UAnonymous _), _ -> false
 
 let glob_sort_eq u1 u2 =
-  glob_sort_expr_eq
+  glob_sort_gen_eq
     (List.equal (fun (x,m) (y,n) -> glob_sort_name_eq x y && Int.equal m n))
     u1 u2
 
 let glob_level_eq u1 u2 =
-  glob_sort_expr_eq glob_sort_name_eq u1 u2
+  glob_sort_gen_eq glob_sort_name_eq u1 u2
 
 let binding_kind_eq bk1 bk2 = match bk1, bk2 with
   | Explicit, Explicit -> true