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