Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | Moving the Tauto tactic to proper Ltac. | 2016-02-22 | |
This gets rid of brittle code written in ML files through Ltac quotations, and reduces the dependance of Coq to such a feature. This also fixes the particular instance of bug #2800, although the underlying issue is still there. |