diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-10-03 17:39:23 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-10-03 17:54:38 +0200 |
| commit | c090d3511eaabe205febc68484b7b0738b403310 (patch) | |
| tree | 085c85ac7dc7fb788d811ee9460bffbcaf476e23 /toplevel/record.mli | |
| parent | 09caa43ae43c0774ea24abb803990d3e70fdc879 (diff) | |
Fixing #3193 (honoring implicit arguments in local definitions).
Diffstat (limited to 'toplevel/record.mli')
0 files changed, 0 insertions, 0 deletions