diff options
author | Pierre Letouzey <pierre.letouzey@inria.fr> | 2017-05-29 18:03:19 +0200 |
---|---|---|
committer | Pierre Letouzey <pierre.letouzey@inria.fr> | 2017-05-29 18:20:05 +0200 |
commit | 2125c92aa9d17b27c9a19a59774e7e319e48262b (patch) | |
tree | 57b6734b6ed307795e0397cd596cecf05a70c66a /kernel/cooking.mli | |
parent | eefda76f6f42674fb342e1aa5f1dcf29569a4806 (diff) |
Omega: use "simpl" only on coefficents, not on atoms (fix #4132)
Two issues in one:
- some focused_simpl were called on the wrong locations
- some focused_simpl were done on whole equations
In the two cases, this could be bad if "simpl" goes too far
with respect to what omega expects: later calls to "occurrence"
might fail. This may happen for instance if an atom isn't a variable,
but a let-in (b:=5:Z in the example).
Diffstat (limited to 'kernel/cooking.mli')
0 files changed, 0 insertions, 0 deletions