diff options
| author | SimonBoulier | 2019-12-02 12:52:39 +0100 |
|---|---|---|
| committer | SimonBoulier | 2020-02-04 16:07:21 +0100 |
| commit | a1d00fa77939f99dd5e7ddd41c8ecf64e8af4fa1 (patch) | |
| tree | 536f901c47c0080a5bc6a2d3b92adaefbfc8490f /pretyping | |
| parent | d07b2862ec9a562f72c2f85e1b5f4529de200a07 (diff) | |
Add syntax for non maximally inserted implicit arguments
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 = |