diff options
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/rawterm.ml | 2 | ||||
| -rw-r--r-- | pretyping/rawterm.mli | 2 |
2 files changed, 2 insertions, 2 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 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 |