aboutsummaryrefslogtreecommitdiffhomepage
path: root/intf/glob_term.mli
diff options
context:
space:
mode:
Diffstat (limited to 'intf/glob_term.mli')
-rw-r--r--intf/glob_term.mli2
1 files changed, 1 insertions, 1 deletions
diff --git a/intf/glob_term.mli b/intf/glob_term.mli
index 832ee4e4b..2a48f3432 100644
--- a/intf/glob_term.mli
+++ b/intf/glob_term.mli
@@ -47,7 +47,7 @@ type glob_constr =
| GRec of Loc.t * fix_kind * Id.t array * glob_decl list array *
glob_constr array * glob_constr array
| GSort of Loc.t * glob_sort
- | GHole of (Loc.t * Evar_kinds.t * Genarg.glob_generic_argument option)
+ | GHole of (Loc.t * Evar_kinds.t * intro_pattern_naming_expr * Genarg.glob_generic_argument option)
| GCast of Loc.t * glob_constr * glob_constr cast_type
and glob_decl = Name.t * binding_kind * glob_constr option * glob_constr