diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-04-06 10:10:03 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-04-30 11:24:53 +0200 |
| commit | edb21eab674b170d125a5b6fbc8213066b356d17 (patch) | |
| tree | 61816200330a54dc74fa3dee3ea71dcf98a561a6 /library/nametab.mli | |
| parent | 991b78fd9627ee76f1a1a39b8460bf361c6af53d (diff) | |
Fixing "decide equality"'s bug #5449.
The code was assuming that the terms t and u for which {t=u}+{t<>u} is
proved were distinct. We refine an internal "generalize" of "u" so
that it works on the two precise occurrences to abstract, even if
other occurrences of u occur as subterm of t too.
We also reuse the global constants found in the statement rather than
reconstructing them (this seems better in case the global constants
eventually get polymorphic universes?).
Diffstat (limited to 'library/nametab.mli')
0 files changed, 0 insertions, 0 deletions