diff options
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/glob_ops.ml | 5 | ||||
| -rw-r--r-- | pretyping/glob_term.ml | 2 |
2 files changed, 4 insertions, 3 deletions
diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml index 02c2fc4a13..0969b3cc03 100644 --- a/pretyping/glob_ops.ml +++ b/pretyping/glob_ops.ml @@ -68,8 +68,9 @@ let glob_sort_eq u1 u2 = match u1, u2 with let binding_kind_eq bk1 bk2 = match bk1, bk2 with | Explicit, Explicit -> true - | Implicit, Implicit -> true - | (Explicit | Implicit), _ -> false + | NonMaxImplicit, NonMaxImplicit -> true + | MaxImplicit, MaxImplicit -> true + | (Explicit | NonMaxImplicit | MaxImplicit), _ -> false let case_style_eq s1 s2 = let open Constr in match s1, s2 with | LetStyle, LetStyle -> true diff --git a/pretyping/glob_term.ml b/pretyping/glob_term.ml index 44323441b6..485a19421d 100644 --- a/pretyping/glob_term.ml +++ b/pretyping/glob_term.ml @@ -65,7 +65,7 @@ and 'a cases_pattern_g = ('a cases_pattern_r, 'a) DAst.t type cases_pattern = [ `any ] cases_pattern_g -type binding_kind = Explicit | Implicit +type binding_kind = Explicit | MaxImplicit | NonMaxImplicit (** Representation of an internalized (or in other words globalized) term. *) type 'a glob_constr_r = |