diff options
author | 2016-04-25 13:20:11 +0200 | |
---|---|---|
committer | 2016-04-27 21:55:45 +0200 | |
commit | 0fc6d2dcdb7d12e37d43cbf44fecaf2c0fddadcc (patch) | |
tree | 16c6f0e9a8816a82da35df6927d4a0a6b4e98693 /test-suite/ide | |
parent | 361cc73acc9d016e183e3fe85a84f470c31bc4e2 (diff) |
Reformatting + removal of some useless data + some cut-elimination
in interning of patterns.
No semantic changes (except the type of ids_of_cases_indtype).
Diffstat (limited to 'test-suite/ide')
0 files changed, 0 insertions, 0 deletions