From 2b80095f5dbfb996643309bfae6f45f62e2ecdb1 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Wed, 18 Nov 2020 13:48:54 +0100
Subject: Reserve "sort_expr" for uninterned universes

---
 pretyping/glob_ops.ml  | 6 +++---
 pretyping/glob_term.ml | 6 +++---
 2 files changed, 6 insertions(+), 6 deletions(-)

(limited to 'pretyping')

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
diff --git a/pretyping/glob_term.ml b/pretyping/glob_term.ml
index a49c8abe26..0b4eab1475 100644
--- a/pretyping/glob_term.ml
+++ b/pretyping/glob_term.ml
@@ -28,15 +28,15 @@ type glob_sort_name =
   | GSet  (** representation of [Set] level *)
   | GType of Libnames.qualid (** representation of a [Type] level *)
 
-type 'a glob_sort_expr =
+type 'a glob_sort_gen =
   | UAnonymous of { rigid : bool } (** not rigid = unifiable by minimization *)
   | UNamed of 'a
 
 (** levels, occurring in universe instances *)
-type glob_level = glob_sort_name glob_sort_expr
+type glob_level = glob_sort_name glob_sort_gen
 
 (** sort expressions *)
-type glob_sort = (glob_sort_name * int) list glob_sort_expr
+type glob_sort = (glob_sort_name * int) list glob_sort_gen
 
 type glob_constraint = glob_sort_name * Univ.constraint_type * glob_sort_name
 
-- 
cgit v1.2.3