diff options
| author | Matthieu Sozeau | 2014-09-23 18:57:08 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2014-09-23 18:57:08 +0200 |
| commit | 01feb4206d26b41bfaab9bd45a7b2fc4db569baf (patch) | |
| tree | 295067c29968d635d5fa7f2a629f72dff718a3c1 /kernel | |
| parent | 13ab2df9ed3a5ea6b7455ea8a7da4341e7f2bcd5 (diff) | |
Fix bug in setoid_rewrite introduced by PMP's commits, which was creating
two versions of the rewriting lemma, keeping useless evars around. This
can now happen only when the rewrite lemma is used under binders... Fix
to do next.
Diffstat (limited to 'kernel')
0 files changed, 0 insertions, 0 deletions