aboutsummaryrefslogtreecommitdiff
path: root/plugins/setoid_ring/Rings_Z.v
AgeCommit message (Expand)Author
2018-03-30Adding some headers, by consistency of style.Hugo Herbelin
2014-05-12Now parsing rules of ML-declared tactics are only made available after thePierre-Marie Pédrot
2012-07-05ZArith + other : favor the use of modern names instead of compat notationsletouzey
2011-08-04moins de reification inutile, noatations standardspottier