diff options
Diffstat (limited to 'pretyping/rawterm.ml')
| -rw-r--r-- | pretyping/rawterm.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/rawterm.ml b/pretyping/rawterm.ml index 47edc73cea..1aeca07cb7 100644 --- a/pretyping/rawterm.ml +++ b/pretyping/rawterm.ml @@ -49,7 +49,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 |