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 /theories/Numbers/NatInt | |
| 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 'theories/Numbers/NatInt')
| -rw-r--r-- | theories/Numbers/NatInt/NZAxioms.v | 4 | ||||
| -rw-r--r-- | theories/Numbers/NatInt/NZDomain.v | 2 |
2 files changed, 2 insertions, 4 deletions
diff --git a/theories/Numbers/NatInt/NZAxioms.v b/theories/Numbers/NatInt/NZAxioms.v index c0f3093291..ff220e7933 100644 --- a/theories/Numbers/NatInt/NZAxioms.v +++ b/theories/Numbers/NatInt/NZAxioms.v @@ -5,8 +5,8 @@ (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* Evgeny Makarov, INRIA, 2007 *) -(************************************************************************) + +(** Initial Author : Evgeny Makarov, INRIA, 2007 *) (*i $Id$ i*) diff --git a/theories/Numbers/NatInt/NZDomain.v b/theories/Numbers/NatInt/NZDomain.v index 60f9287c84..2d627dbc79 100644 --- a/theories/Numbers/NatInt/NZDomain.v +++ b/theories/Numbers/NatInt/NZDomain.v @@ -5,8 +5,6 @@ (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* Evgeny Makarov, INRIA, 2007 *) -(************************************************************************) (*i $Id$ i*) |