aboutsummaryrefslogtreecommitdiff
path: root/theories/Init/Tauto.v
AgeCommit message (Expand)Author
2020-04-21Moving the main Require Export Ltac in Prelude.v.Hugo Herbelin
2017-10-19Moving bug numbers to BZ# format in the source code.Théo Zimmermann
2017-06-15plugins/ltac : avoid spurious .cmxs filesPierre Letouzey
2016-02-23Moving tauto.ml4 to a proper ML file.Pierre-Marie Pédrot
2016-02-22Moving the Tauto tactic to proper Ltac.Pierre-Marie Pédrot