diff options
| author | Cyprien Mangin | 2016-06-30 19:42:55 +0200 |
|---|---|---|
| committer | Cyprien Mangin | 2016-06-30 19:52:18 +0200 |
| commit | 4b61c0693d453dd0026792185354d68ba1db9022 (patch) | |
| tree | 744808e201651e933bc812a945edda7fe8749d30 /kernel/type_errors.mli | |
| parent | fd47b2d2638518fe62ce9c63557d2dab219d9558 (diff) | |
Update the documentation for goal selectors.
Diffstat (limited to 'kernel/type_errors.mli')
0 files changed, 0 insertions, 0 deletions