| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2019-03-26 | [evarconv] solve_simple_eqn is weaker than miller pattern (fix #9663) | Enrico Tassi | |
| In particular evar_eqappr_x tries to find a miller pattern on both sides, while the fast path for evars tries solve_simple_eqn in one direction only. So if you have (Evar-not-miller = Evar-miller) the code was not trying to solve the RHS. | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |