diff options
| author | Enrico Tassi | 2016-06-17 16:26:59 +0200 |
|---|---|---|
| committer | Enrico Tassi | 2016-06-17 16:27:35 +0200 |
| commit | 8a45a3a5d08f9e9339d0ba9cc9624a895d4cfc57 (patch) | |
| tree | 84d49919537123dd73464899cbfbe0e0a5f069ba /kernel/type_errors.mli | |
| parent | 57a3f38832dba3a9b7a1de146bd45451227a03e8 (diff) | |
Mentioning goal selectors in CHANGES
Diffstat (limited to 'kernel/type_errors.mli')
0 files changed, 0 insertions, 0 deletions