diff options
| author | Maxime Dénès | 2018-05-16 15:25:07 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2018-05-16 15:25:07 +0200 |
| commit | 19e24bf1f5eefee37ee2648c04844b5ea3ca2ab2 (patch) | |
| tree | 60ae3d8527f10aa5e198639139364bdaebddf821 /pretyping/pretype_errors.ml | |
| parent | 3f480c993311d19b152deb6bb4dc561188d76fc7 (diff) | |
| parent | e266976abc8c170c1e4bf1c98629c190b844f1ab (diff) | |
Merge PR #7391: Add a small documentation writer's guide
Diffstat (limited to 'pretyping/pretype_errors.ml')
0 files changed, 0 insertions, 0 deletions