diff options
| author | Matthieu Sozeau | 2020-03-01 13:11:20 +0100 |
|---|---|---|
| committer | Matthieu Sozeau | 2020-03-01 13:40:29 +0100 |
| commit | 50de1d310fb5a0d94fe7449f622fb5c4b751a46c (patch) | |
| tree | 635b10c639066cf6ff14743d2cca48b7e5b2136c /plugins | |
| parent | aeca986089d005054496ed4bcf1b920e8fa02173 (diff) | |
Fix mishandling of sigma in guess_elim (regression from 8.11)
In case no eliminator is given, we wait until `get_eliminator` to
produce the actual eliminator. Using the sigma produced by guess_elim
here would insert an unused universe for the predicate's type in the
sigma.
Diffstat (limited to 'plugins')
0 files changed, 0 insertions, 0 deletions