Leonardo de Moura f8d472c9f1 feat(frontends/lean/parse_rewrite_tactic): change the semantics of rewrite[↑f] when f is recursive ... After this commit it behaves like 'unfold f'. That is, it will unfold f even if it fails to fold recursive applications. Now, only 'esimp[f]' will not unfold f-applications when it cannot fold the recursive applications. This commit also closes #692. It is part of a series of commits that addresses this issue. closes #692		2015-07-12 13:20:21 -04:00
..
lean	feat(frontends/lean/parse_rewrite_tactic): change the semantics of rewrite[↑f] when f is recursive	2015-07-12 13:20:21 -04:00
lua	chore(library/coercion): remove lua bindings for coercion module	2015-07-01 14:08:49 -07:00