diff options
| author | Hugo Herbelin | 2020-08-22 12:50:48 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2020-08-28 15:34:00 +0200 |
| commit | 1a91771fdc26bd0260ff26aceb91070217717d3b (patch) | |
| tree | 0aec8f289eb7da44dfb1e38f205282ebbc2804aa /doc/plugin_tutorial/tuto1/src/simple_check.ml | |
| parent | 699eb941cbdd2b3caf98f18b2d49b249b598ca1b (diff) | |
When printing the type in About, use the renamed arguments.
Diffstat (limited to 'doc/plugin_tutorial/tuto1/src/simple_check.ml')
0 files changed, 0 insertions, 0 deletions