diff options
| author | Hugo Herbelin | 2020-08-10 20:14:47 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2020-08-20 21:26:36 +0200 |
| commit | 13e4331494ea5bd2b37cb5730ac15662a9067772 (patch) | |
| tree | 3d2e0d3488242fec234411e448047cd75a75b26a /dev/bench | |
| parent | 609152467f4d717713b7ea700f5155fc9f341cd7 (diff) | |
Quick fix to #12787 (injection anomaly due to inconsistent comp. of free vars).
We fix it by reducing K-redexes the same in the both places
(make_tuple and minimal_free_rels) which compute the dependencies of a
dependent equality.
Diffstat (limited to 'dev/bench')
0 files changed, 0 insertions, 0 deletions