diff options
Diffstat (limited to 'interp/topconstr.ml')
| -rw-r--r-- | interp/topconstr.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/interp/topconstr.ml b/interp/topconstr.ml index cef1b93915..570eae7e56 100644 --- a/interp/topconstr.ml +++ b/interp/topconstr.ml @@ -590,7 +590,7 @@ type notation = string type explicitation = ExplByPos of int * identifier option | ExplByName of identifier -type binder_kind = Default of binding_kind | TypeClass of binding_kind +type binder_kind = Default of binding_kind | TypeClass of binding_kind * binding_kind type proj_flag = int option (* [Some n] = proj of the n-th visible argument *) |