diff options
| -rw-r--r-- | pretyping/glob_ops.ml | 6 | ||||
| -rw-r--r-- | pretyping/glob_term.ml | 6 | ||||
| -rw-r--r-- | vernac/vernacexpr.ml | 6 |
3 files changed, 8 insertions, 10 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 diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml index defb0691c0..89c09bb169 100644 --- a/vernac/vernacexpr.ml +++ b/vernac/vernacexpr.ml @@ -129,8 +129,6 @@ type option_setting = (** Identifier and optional list of bound universes and constraints. *) -type sort_expr = Sorts.family - type definition_expr = | ProveBody of local_binder_expr list * constr_expr | DefineBody of local_binder_expr list * Genredexpr.raw_red_expr option * constr_expr @@ -210,8 +208,8 @@ type proof_end = | Proved of opacity_flag * lident option type scheme = - | InductionScheme of bool * qualid or_by_notation * sort_expr - | CaseScheme of bool * qualid or_by_notation * sort_expr + | InductionScheme of bool * qualid or_by_notation * Sorts.family + | CaseScheme of bool * qualid or_by_notation * Sorts.family | EqualityScheme of qualid or_by_notation type section_subset_expr = |