aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Init/Tauto.v
Commit message (Expand)AuthorAge
* Moving tauto.ml4 to a proper ML file.Gravatar Pierre-Marie Pédrot2016-02-23
* Moving the Tauto tactic to proper Ltac.Gravatar Pierre-Marie Pédrot2016-02-22