diff options
| author | Maxime Dénès | 2016-11-08 09:36:42 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2016-11-08 09:36:42 +0100 |
| commit | c60d155c2213461b8e4392b729445486086302d9 (patch) | |
| tree | 4427c368a62c3d96be19f31b7d425766fbabe5c5 /kernel/type_errors.ml | |
| parent | b58f5b2b499b687288587837cbf0cfc04a269c75 (diff) | |
Update documentation of Arguments after recent changes.
Diffstat (limited to 'kernel/type_errors.ml')
0 files changed, 0 insertions, 0 deletions