diff options
Diffstat (limited to 'pretyping/glob_term.ml')
| -rw-r--r-- | pretyping/glob_term.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/pretyping/glob_term.ml b/pretyping/glob_term.ml index 7c859a5332..10e9d60fd5 100644 --- a/pretyping/glob_term.ml +++ b/pretyping/glob_term.ml @@ -17,7 +17,6 @@ arguments and pattern-matching compilation are not. *) open Names -open Decl_kinds type existential_name = Id.t @@ -66,6 +65,8 @@ and 'a cases_pattern_g = ('a cases_pattern_r, 'a) DAst.t type cases_pattern = [ `any ] cases_pattern_g +type binding_kind = Explicit | Implicit + (** Representation of an internalized (or in other words globalized) term. *) type 'a glob_constr_r = | GRef of GlobRef.t * glob_level list option |