diff options
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/glob_ops.ml | 6 | ||||
| -rw-r--r-- | pretyping/glob_term.ml | 6 |
2 files changed, 6 insertions, 6 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 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 |