| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2018-10-04 | rename test files (do not start by a digit) | Vincent Laporte | |
| 2017-05-29 | Omega: use "simpl" only on coefficents, not on atoms (fix #4132) | Pierre Letouzey | |
| 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). | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |