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 /plugins | |
| 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 'plugins')
| -rw-r--r-- | plugins/micromega/coq_micromega.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml index d4bafe773f..7adae148bd 100644 --- a/plugins/micromega/coq_micromega.ml +++ b/plugins/micromega/coq_micromega.ml @@ -846,7 +846,7 @@ struct match env with | [] -> ([v],n) | e::l -> - if EConstr.eq_constr sigma e v + if EConstr.eq_constr_nounivs sigma e v then (env,n) else let (env,n) = _add l ( n+1) v in |