aboutsummaryrefslogtreecommitdiff
path: root/theories/ZArith/ZOdiv.v
AgeCommit message (Expand)Author
2010-11-10Integer division: quot and rem (trunc convention) in addition to div and modletouzey
2010-10-14Numbers: new functions pow, even, odd + many reorganisationsletouzey
2010-07-24Updated all headers for 8.3 and trunkherbelin
2010-02-10Euclidean division for NArithletouzey
2010-02-09ZBinary (impl of Numbers via Z) reworked, comes earlier, subsumes ZOrderedTypeletouzey
2010-01-11Support "Local Obligation Tactic" (now the default in sections).msozeau
2010-01-07Rework of GenericMinMax: new axiomatic, split logical/decidable parts, Leibni...letouzey
2010-01-05Numbers abstract layer: more Module Type, used especially for divisions.letouzey
2009-12-17ZOdiv: fully use generic properties from ZDivTrunc.vletouzey
2009-12-17Division in Numbers : more properties, new filenames based on a paper by R. B...letouzey
2009-12-16Division in Numbers: more properties proved (still W.I.P.)letouzey
2009-12-15A generic euclidean division in Numbers (Still Work-In-Progress)letouzey
2009-09-17Delete trailing whitespaces in all *.{v,ml*} filesglondu
2009-09-09Znumtheory + Zdiv enriched with stuff from ZMicromega, misc improvementsletouzey
2007-11-10A result about Zsgn(a/b), both for Zdiv and ZOdivletouzey
2007-11-10First reasonably complete version of ZOdiv, including some propertiesletouzey
2007-11-09git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10309 85f007b7-540e-0...jforest
2007-11-09more about ZOdiv and ZOmod (still not finished)letouzey
2007-11-08setoid_ring/Ring_zdiv is moved to ZArith and renamed to ZOdiv_def. letouzey