diff options
| author | Matthieu Sozeau | 2016-05-09 17:43:59 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2016-07-04 15:48:15 +0200 |
| commit | ee8009e05d3e782ee6333d0054ee2fce5cda89a4 (patch) | |
| tree | 036354fdce7a9ab08e98dbddfc5eebad65b03106 /kernel | |
| parent | a5b631f7260e7d29defd8bd5c67db543742c9ecd (diff) | |
congruence: remove casts of indexed terms
This fixes the end of bug #4069, provoked by a use
of unshelve refine which introduces a cast.
Diffstat (limited to 'kernel')
0 files changed, 0 insertions, 0 deletions