diff options
| author | Pierre-Marie Pédrot | 2019-03-05 22:41:24 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-03-05 22:41:24 +0100 |
| commit | a83eac8463787c13a2dbd3903baf2b59ca1a4635 (patch) | |
| tree | b7c70b701c0667808f3f4a2e40964ea5da358667 /kernel/type_errors.ml | |
| parent | 73550d2c6feaa86447da94f7010a1ea6a04fb39a (diff) | |
| parent | b08c14e551def3fb1ec885cf1ff05018f3d87ab9 (diff) | |
Merge PR #9524: Fix #7632: Change syntax of autoapply according to the documentation.
Reviewed-by: ppedrot
Diffstat (limited to 'kernel/type_errors.ml')
0 files changed, 0 insertions, 0 deletions