diff options
| author | letouzey | 2009-12-17 16:46:54 +0000 |
|---|---|---|
| committer | letouzey | 2009-12-17 16:46:54 +0000 |
| commit | 35e84a95326c95f9399084c843e244de6ae25753 (patch) | |
| tree | 46051f847373a93c6cd9c79b583503e79af1f9bb /dev | |
| parent | 622dbc2eb726949cda5c44639250336586ed8379 (diff) | |
Division in Numbers : more properties, new filenames based on a paper by R. Boute
Following R. Boute (paper "the Euclidean Definition of the Functions div and mod"):
- ZDivFloor.v for Coq historical division (former ZDivCoq.v)
- ZDivTrunc.v for Ocaml convention (former ZDivOcaml.v)
- ZDivEucl.v for "Mathematical" convention 0<=r (former ZDivMath.v)
These property functors are more or less finished (except that sign and abs
stuff should be migrated to a separate file).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12594 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions