diff options
| author | Hugo Herbelin | 2020-02-25 07:55:49 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2020-02-25 09:03:44 +0100 |
| commit | f71ec3907c0535bf6831ed60a3656ecbe8ac744f (patch) | |
| tree | f0e3aae3924d5eb1a73895601c497bb0a9ec9dfb /kernel/nativelib.mli | |
| parent | da984ceafbb450dc5a9fe8f8971d8c90a060f233 (diff) | |
Fixing residual bug of #11120.
On the principle that a notation to a constant inherits the implicit
arguments of the constant, a non-applied notation should inherit its
next maximal implicit arguments.
Diffstat (limited to 'kernel/nativelib.mli')
0 files changed, 0 insertions, 0 deletions