aboutsummaryrefslogtreecommitdiff
path: root/plugins/setoid_ring/InitialRing.v
AgeCommit message (Expand)Author
2014-05-06This commit adds full universe polymorphism and fast projections to Coq.Matthieu Sozeau
2014-02-08Less dependencies in Omega.Pierre-Marie Pédrot
2012-08-08Updating headers.herbelin
2012-07-05Kills the useless tactic annotations "in |- *"letouzey
2012-07-05ZArith + other : favor the use of modern names instead of compat notationsletouzey
2011-06-28Some cleanup of Zdiv and Zquot, deletion of useless Zdiv_defletouzey
2011-05-05BinInt: Z.add become the alternative Z.add'letouzey
2011-05-05Setoid_ring: some cleanups related with BinPos and BinNatletouzey
2011-05-05Modularization of BinPos + fixes in Stdlibletouzey
2010-11-10Integer division: quot and rem (trunc convention) in addition to div and modletouzey
2010-09-20Added eta-expansion in kernel, type inference and tactic unification,herbelin
2010-07-24Updated all headers for 8.3 and trunkherbelin
2010-02-10Euclidean division for NArithletouzey
2009-09-17Delete trailing whitespaces in all *.{v,ml*} filesglondu
2009-03-20Directory 'contrib' renamed into 'plugins', to end confusion with archive of ...letouzey