aboutsummaryrefslogtreecommitdiff
path: root/plugins/setoid_ring/RealField.v
AgeCommit message (Expand)Author
2012-07-05Kills the useless tactic annotations "in |- *"letouzey
2012-07-05Open Local Scope ---> Local Open Scope, same with Notation and aliiletouzey
2012-07-05ZArith + other : favor the use of modern names instead of compat notationsletouzey
2009-09-17Delete trailing whitespaces in all *.{v,ml*} filesglondu
2009-03-20Directory 'contrib' renamed into 'plugins', to end confusion with archive of ...letouzey