diff options
| author | Gabriel Scherer | 2015-06-27 22:37:23 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2016-06-27 12:57:30 +0200 |
| commit | ed015ec083e298b2e65b7b61fcf924642d438ee4 (patch) | |
| tree | fcbf03ebad77820b4fa7b2414588efa109f9e235 /kernel/nativelib.ml | |
| parent | 5a212ff444e9e231f5b56629e5cf15087bac69c6 (diff) | |
minor: interp/constrintern.ml, clarify field completion
The type of the user-defined function "completer" changes to be
simpler and better reflect its purpose: provide values for missing
field assignments. In the future we may want to also pass the name of
the field as parameter (currently only the index is given, and both
uses of the function ignore it), in particular if we want to implement
{ r with x = ...; y = ... }.
Diffstat (limited to 'kernel/nativelib.ml')
0 files changed, 0 insertions, 0 deletions