diff options
| author | Pierre-Marie Pédrot | 2015-11-11 18:45:32 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2015-11-11 18:45:32 +0100 |
| commit | 701a69732ef2abfc7384296e090a3e9bd7604bbd (patch) | |
| tree | 356247eb62159a080e343fef087a7cb705d6a0ea /kernel/type_errors.mli | |
| parent | ab1d8792143a05370a1efe3d19469c25b82d7097 (diff) | |
Fixing bug #3554: Anomaly: Anonymous implicit argument.
We just handle unnamed implicits using a dummy name. Note that the implicit
argument logic should still output warnings whenever the user writes implicit
arguments that won't be taken into account, but I'll leave that for another
time.
Diffstat (limited to 'kernel/type_errors.mli')
0 files changed, 0 insertions, 0 deletions