aboutsummaryrefslogtreecommitdiff
path: root/plugins/setoid_ring/RealField.v
AgeCommit message (Expand)Author
2019-06-17Update ml-style headers to new year.Théo Zimmermann
2019-04-02Make R parser parse decimals (e.g., 1.02e+01)Pierre Roux
2018-03-30Adding some headers, by consistency of style.Hugo Herbelin
2017-03-22Change the parser and printer so that they use IZR for real constants.Guillaume Melquiond
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