diff options
| author | Hugo Herbelin | 2016-04-25 13:20:11 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2016-04-27 21:55:45 +0200 |
| commit | 0fc6d2dcdb7d12e37d43cbf44fecaf2c0fddadcc (patch) | |
| tree | 16c6f0e9a8816a82da35df6927d4a0a6b4e98693 /pretyping | |
| 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 'pretyping')
0 files changed, 0 insertions, 0 deletions