aboutsummaryrefslogtreecommitdiff
path: root/plugins/omega/PreOmega.v
AgeCommit message (Expand)Author
2018-02-27Update headers following #6543.Théo Zimmermann
2018-02-14Extend `zify_N` with knowledge about `N.pred`Joachim Breitner
2017-07-04Bump year in headers.Pierre-Marie Pédrot
2017-06-12zify: force reduction of (Z.max 0 0) and similar (fix #5439)Pierre Letouzey
2017-06-12zify: confusion between Pos2Z.inj_sub and Pos2Z.inj_sub_max (fix #5336)Pierre Letouzey
2017-06-01Fix bug #5019 (looping zify on dependent types)Jason Gross
2016-01-20Update copyright headers.Maxime Dénès
2015-01-12Update headers.Maxime Dénès
2012-10-01Ltac repeat is in fact already doing progressletouzey
2012-08-08Updating headers.herbelin
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
2011-09-06Improved ltac code for zify (fix #2575).letouzey
2011-05-05Modularization of BinPos + fixes in Stdlibletouzey
2009-09-17Delete trailing whitespaces in all *.{v,ml*} filesglondu
2009-03-20Directory 'contrib' renamed into 'plugins', to end confusion with archive of ...letouzey