aboutsummaryrefslogtreecommitdiffhomepage
path: root/intf/notation_term.mli
diff options
context:
space:
mode:
Diffstat (limited to 'intf/notation_term.mli')
-rw-r--r--intf/notation_term.mli2
1 files changed, 1 insertions, 1 deletions
diff --git a/intf/notation_term.mli b/intf/notation_term.mli
index daf605ab2..5d9c1c177 100644
--- a/intf/notation_term.mli
+++ b/intf/notation_term.mli
@@ -24,7 +24,7 @@ type notation_constr =
| NRef of global_reference
| NVar of Id.t
| NApp of notation_constr * notation_constr list
- | NHole of Evar_kinds.t * Genarg.glob_generic_argument option
+ | NHole of Evar_kinds.t * Misctypes.intro_pattern_naming_expr * Genarg.glob_generic_argument option
| NList of Id.t * Id.t * notation_constr * notation_constr * bool
(** Part only in [glob_constr] *)
| NLambda of Name.t * notation_constr * notation_constr