diff options
| author | Pierre-Marie Pédrot | 2016-01-16 23:19:40 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-01-17 00:35:15 +0100 |
| commit | e6b05180d789fb46bc91c71bc97efaf8b552f0fd (patch) | |
| tree | 563f63a45af2e9a8d247656836dea9290209585e /lib/genarg.mli | |
| parent | 8a3b19b62720e2324ef24003407c2e83335a51a5 (diff) | |
ML extensions use untyped representation of user entries.
Diffstat (limited to 'lib/genarg.mli')
0 files changed, 0 insertions, 0 deletions