diff options
| author | Pierre-Marie Pédrot | 2018-12-30 17:20:41 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-12-30 17:23:04 +0100 |
| commit | 5ff1fc8b41e8265af7e1c1c91d137ec88f2b04d0 (patch) | |
| tree | 2f95a38bb5fa55387e41fe557052f5a95d6e13d2 /kernel | |
| parent | 2760bdc584d3b49d9ebcd2052c6be13e08cb1429 (diff) | |
Do not take universes into account in lia reification.
This is slightly blunt, it might be the case that we get delayed constraints
that cannot be solved resulting in a later universe inconsistency, but it looks
highly unlikely on arithmetical statements.
Alternatively we would have threaded the unification state, but this would
have required a much deeper change.
Fixes #9268.
Diffstat (limited to 'kernel')
0 files changed, 0 insertions, 0 deletions
