diff options
| author | letouzey | 2010-04-29 13:50:31 +0000 |
|---|---|---|
| committer | letouzey | 2010-04-29 13:50:31 +0000 |
| commit | af93e4cf8b1a839d21499b3b9737bb8904edcae8 (patch) | |
| tree | b9a4f28e6f8106bcf19e017f64147f836f810c4b /theories/Numbers/Integer | |
| parent | 0f61b02f84b41e1f019cd78824de28f18ff854aa (diff) | |
Remove the svn-specific $Id$ annotations
- Many of them were broken, some of them after Pierre B's rework
of mli for ocamldoc, but not only (many bad annotation, many files
with no svn property about Id, etc)
- Useless for those of us that work with git-svn (and a fortiori
in a forthcoming git-only setting)
- Even in svn, they seem to be of little interest
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12972 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Numbers/Integer')
| -rw-r--r-- | theories/Numbers/Integer/Abstract/ZAdd.v | 2 | ||||
| -rw-r--r-- | theories/Numbers/Integer/Abstract/ZAddOrder.v | 2 | ||||
| -rw-r--r-- | theories/Numbers/Integer/Abstract/ZAxioms.v | 2 | ||||
| -rw-r--r-- | theories/Numbers/Integer/Abstract/ZBase.v | 2 | ||||
| -rw-r--r-- | theories/Numbers/Integer/Abstract/ZLt.v | 2 | ||||
| -rw-r--r-- | theories/Numbers/Integer/Abstract/ZMul.v | 2 | ||||
| -rw-r--r-- | theories/Numbers/Integer/Abstract/ZMulOrder.v | 2 | ||||
| -rw-r--r-- | theories/Numbers/Integer/Abstract/ZProperties.v | 2 | ||||
| -rw-r--r-- | theories/Numbers/Integer/BigZ/BigZ.v | 2 | ||||
| -rw-r--r-- | theories/Numbers/Integer/BigZ/ZMake.v | 2 | ||||
| -rw-r--r-- | theories/Numbers/Integer/Binary/ZBinary.v | 2 | ||||
| -rw-r--r-- | theories/Numbers/Integer/NatPairs/ZNatPairs.v | 2 | ||||
| -rw-r--r-- | theories/Numbers/Integer/SpecViaZ/ZSig.v | 2 | ||||
| -rw-r--r-- | theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v | 2 |
14 files changed, 0 insertions, 28 deletions
diff --git a/theories/Numbers/Integer/Abstract/ZAdd.v b/theories/Numbers/Integer/Abstract/ZAdd.v index 5663408d1b..123c40428b 100644 --- a/theories/Numbers/Integer/Abstract/ZAdd.v +++ b/theories/Numbers/Integer/Abstract/ZAdd.v @@ -8,8 +8,6 @@ (* Evgeny Makarov, INRIA, 2007 *) (************************************************************************) -(*i $Id$ i*) - Require Export ZBase. Module ZAddPropFunct (Import Z : ZAxiomsSig'). diff --git a/theories/Numbers/Integer/Abstract/ZAddOrder.v b/theories/Numbers/Integer/Abstract/ZAddOrder.v index de12993f89..adc8432646 100644 --- a/theories/Numbers/Integer/Abstract/ZAddOrder.v +++ b/theories/Numbers/Integer/Abstract/ZAddOrder.v @@ -8,8 +8,6 @@ (* Evgeny Makarov, INRIA, 2007 *) (************************************************************************) -(*i $Id$ i*) - Require Export ZLt. Module ZAddOrderPropFunct (Import Z : ZAxiomsSig'). diff --git a/theories/Numbers/Integer/Abstract/ZAxioms.v b/theories/Numbers/Integer/Abstract/ZAxioms.v index 9158a214da..46f7810ac9 100644 --- a/theories/Numbers/Integer/Abstract/ZAxioms.v +++ b/theories/Numbers/Integer/Abstract/ZAxioms.v @@ -8,8 +8,6 @@ (* Evgeny Makarov, INRIA, 2007 *) (************************************************************************) -(*i $Id$ i*) - Require Export NZAxioms. Set Implicit Arguments. diff --git a/theories/Numbers/Integer/Abstract/ZBase.v b/theories/Numbers/Integer/Abstract/ZBase.v index 44bb02ecc6..ca288e6b2a 100644 --- a/theories/Numbers/Integer/Abstract/ZBase.v +++ b/theories/Numbers/Integer/Abstract/ZBase.v @@ -8,8 +8,6 @@ (* Evgeny Makarov, INRIA, 2007 *) (************************************************************************) -(*i $Id$ i*) - Require Export Decidable. Require Export ZAxioms. Require Import NZProperties. diff --git a/theories/Numbers/Integer/Abstract/ZLt.v b/theories/Numbers/Integer/Abstract/ZLt.v index 849bf6b407..fdb7c77f66 100644 --- a/theories/Numbers/Integer/Abstract/ZLt.v +++ b/theories/Numbers/Integer/Abstract/ZLt.v @@ -8,8 +8,6 @@ (* Evgeny Makarov, INRIA, 2007 *) (************************************************************************) -(*i $Id$ i*) - Require Export ZMul. Module ZOrderPropFunct (Import Z : ZAxiomsSig'). diff --git a/theories/Numbers/Integer/Abstract/ZMul.v b/theories/Numbers/Integer/Abstract/ZMul.v index 84d840ad20..4a87a54c82 100644 --- a/theories/Numbers/Integer/Abstract/ZMul.v +++ b/theories/Numbers/Integer/Abstract/ZMul.v @@ -8,8 +8,6 @@ (* Evgeny Makarov, INRIA, 2007 *) (************************************************************************) -(*i $Id$ i*) - Require Export ZAdd. Module ZMulPropFunct (Import Z : ZAxiomsSig'). diff --git a/theories/Numbers/Integer/Abstract/ZMulOrder.v b/theories/Numbers/Integer/Abstract/ZMulOrder.v index 99be58ebd8..1952f4e2a1 100644 --- a/theories/Numbers/Integer/Abstract/ZMulOrder.v +++ b/theories/Numbers/Integer/Abstract/ZMulOrder.v @@ -8,8 +8,6 @@ (* Evgeny Makarov, INRIA, 2007 *) (************************************************************************) -(*i $Id$ i*) - Require Export ZAddOrder. Module Type ZMulOrderPropFunct (Import Z : ZAxiomsSig'). diff --git a/theories/Numbers/Integer/Abstract/ZProperties.v b/theories/Numbers/Integer/Abstract/ZProperties.v index 45662d3b66..76451da33f 100644 --- a/theories/Numbers/Integer/Abstract/ZProperties.v +++ b/theories/Numbers/Integer/Abstract/ZProperties.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - Require Export ZAxioms ZMaxMin ZSgnAbs. (** This functor summarizes all known facts about Z. diff --git a/theories/Numbers/Integer/BigZ/BigZ.v b/theories/Numbers/Integer/BigZ/BigZ.v index aa62ae76bf..c0b8074b69 100644 --- a/theories/Numbers/Integer/BigZ/BigZ.v +++ b/theories/Numbers/Integer/BigZ/BigZ.v @@ -8,8 +8,6 @@ (* Benjamin Gregoire, Laurent Thery, INRIA, 2007 *) (************************************************************************) -(*i $Id$ i*) - Require Export BigN. Require Import ZProperties ZDivFloor ZSig ZSigZAxioms ZMake. diff --git a/theories/Numbers/Integer/BigZ/ZMake.v b/theories/Numbers/Integer/BigZ/ZMake.v index 3196f11ea9..41b1d6e697 100644 --- a/theories/Numbers/Integer/BigZ/ZMake.v +++ b/theories/Numbers/Integer/BigZ/ZMake.v @@ -8,8 +8,6 @@ (* Benjamin Gregoire, Laurent Thery, INRIA, 2007 *) (************************************************************************) -(*i $Id$ i*) - Require Import ZArith. Require Import BigNumPrelude. Require Import NSig. diff --git a/theories/Numbers/Integer/Binary/ZBinary.v b/theories/Numbers/Integer/Binary/ZBinary.v index bc1dadcd9e..aa857f3ca7 100644 --- a/theories/Numbers/Integer/Binary/ZBinary.v +++ b/theories/Numbers/Integer/Binary/ZBinary.v @@ -8,8 +8,6 @@ (* Evgeny Makarov, INRIA, 2007 *) (************************************************************************) -(*i $Id$ i*) - Require Import ZAxioms ZProperties. Require Import BinInt Zcompare Zorder ZArith_dec Zbool. diff --git a/theories/Numbers/Integer/NatPairs/ZNatPairs.v b/theories/Numbers/Integer/NatPairs/ZNatPairs.v index 8b5624cdf8..cafcc549e3 100644 --- a/theories/Numbers/Integer/NatPairs/ZNatPairs.v +++ b/theories/Numbers/Integer/NatPairs/ZNatPairs.v @@ -8,8 +8,6 @@ (* Evgeny Makarov, INRIA, 2007 *) (************************************************************************) -(*i $Id$ i*) - Require Import NProperties. (* The most complete file for N *) Require Export ZProperties. (* The most complete file for Z *) Require Export Ring. diff --git a/theories/Numbers/Integer/SpecViaZ/ZSig.v b/theories/Numbers/Integer/SpecViaZ/ZSig.v index ffa91706f7..ab12e584b6 100644 --- a/theories/Numbers/Integer/SpecViaZ/ZSig.v +++ b/theories/Numbers/Integer/SpecViaZ/ZSig.v @@ -8,8 +8,6 @@ (* Benjamin Gregoire, Laurent Thery, INRIA, 2007 *) (************************************************************************) -(*i $Id$ i*) - Require Import ZArith Znumtheory. Open Scope Z_scope. diff --git a/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v b/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v index bcecb6a8a2..2c4797969d 100644 --- a/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v +++ b/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - Require Import ZArith ZAxioms ZDivFloor ZSig. (** * The interface [ZSig.ZType] implies the interface [ZAxiomsSig] |
