diff options
| author | Regis-Gianas | 2014-11-04 12:09:07 +0100 |
|---|---|---|
| committer | Regis-Gianas | 2014-11-04 22:51:36 +0100 |
| commit | d3b4b78faced5dae3c4b8f2b05dc40375a7a6d91 (patch) | |
| tree | 3943487bcb7c6d50d3b3b1f0824ae318e1ea05fa /kernel/type_errors.ml | |
| parent | 99eb8aa251328a42324455460ecc20aa0cbae046 (diff) | |
lib/Xml_parser.parse: Publish and document new interface.
Diffstat (limited to 'kernel/type_errors.ml')
0 files changed, 0 insertions, 0 deletions