diff options
| author | Cyprien Mangin | 2016-06-03 09:57:20 +0200 |
|---|---|---|
| committer | Cyprien Mangin | 2016-06-14 06:21:30 +0200 |
| commit | 9356f42d5f84f9b325f71bab041d1b8184384a21 (patch) | |
| tree | 15031e5d024e6925d65bcac5c8b0c3fd21b8b4be /kernel/type_errors.mli | |
| parent | 1e19f163b8c7a21d63165784828f4d733aa95171 (diff) | |
Remove the need for brackets in goal selectors.
Diffstat (limited to 'kernel/type_errors.mli')
0 files changed, 0 insertions, 0 deletions