diff options
Diffstat (limited to 'pretyping/rawterm.mli')
| -rw-r--r-- | pretyping/rawterm.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/rawterm.mli b/pretyping/rawterm.mli index 29237a675b..54bb306bd0 100644 --- a/pretyping/rawterm.mli +++ b/pretyping/rawterm.mli @@ -47,7 +47,7 @@ type 'a bindings = type 'a with_bindings = 'a * 'a bindings type hole_kind = - | ImplicitArg of global_reference * int + | ImplicitArg of global_reference * (int * identifier option) | BinderType of name | QuestionMark | CasesType |