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/Natural | |
| 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/Natural')
| -rw-r--r-- | theories/Numbers/Natural/Abstract/NAdd.v | 2 | ||||
| -rw-r--r-- | theories/Numbers/Natural/Abstract/NAddOrder.v | 2 | ||||
| -rw-r--r-- | theories/Numbers/Natural/Abstract/NAxioms.v | 2 | ||||
| -rw-r--r-- | theories/Numbers/Natural/Abstract/NBase.v | 2 | ||||
| -rw-r--r-- | theories/Numbers/Natural/Abstract/NDefOps.v | 2 | ||||
| -rw-r--r-- | theories/Numbers/Natural/Abstract/NIso.v | 2 | ||||
| -rw-r--r-- | theories/Numbers/Natural/Abstract/NMulOrder.v | 2 | ||||
| -rw-r--r-- | theories/Numbers/Natural/Abstract/NOrder.v | 2 | ||||
| -rw-r--r-- | theories/Numbers/Natural/Abstract/NProperties.v | 2 | ||||
| -rw-r--r-- | theories/Numbers/Natural/Abstract/NStrongRec.v | 2 | ||||
| -rw-r--r-- | theories/Numbers/Natural/Abstract/NSub.v | 2 | ||||
| -rw-r--r-- | theories/Numbers/Natural/BigN/NMake_gen.ml | 2 | ||||
| -rw-r--r-- | theories/Numbers/Natural/BigN/Nbasic.v | 2 | ||||
| -rw-r--r-- | theories/Numbers/Natural/Binary/NBinary.v | 2 | ||||
| -rw-r--r-- | theories/Numbers/Natural/Peano/NPeano.v | 2 | ||||
| -rw-r--r-- | theories/Numbers/Natural/SpecViaZ/NSig.v | 2 | ||||
| -rw-r--r-- | theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v | 2 |
17 files changed, 0 insertions, 34 deletions
diff --git a/theories/Numbers/Natural/Abstract/NAdd.v b/theories/Numbers/Natural/Abstract/NAdd.v index 9f0b54a6a2..8596412807 100644 --- a/theories/Numbers/Natural/Abstract/NAdd.v +++ b/theories/Numbers/Natural/Abstract/NAdd.v @@ -8,8 +8,6 @@ (* Evgeny Makarov, INRIA, 2007 *) (************************************************************************) -(*i $Id$ i*) - Require Export NBase. Module NAddPropFunct (Import N : NAxiomsSig'). diff --git a/theories/Numbers/Natural/Abstract/NAddOrder.v b/theories/Numbers/Natural/Abstract/NAddOrder.v index 0ce04e54eb..67bc808507 100644 --- a/theories/Numbers/Natural/Abstract/NAddOrder.v +++ b/theories/Numbers/Natural/Abstract/NAddOrder.v @@ -8,8 +8,6 @@ (* Evgeny Makarov, INRIA, 2007 *) (************************************************************************) -(*i $Id$ i*) - Require Export NOrder. Module NAddOrderPropFunct (Import N : NAxiomsSig'). diff --git a/theories/Numbers/Natural/Abstract/NAxioms.v b/theories/Numbers/Natural/Abstract/NAxioms.v index 42016ab10b..cd3d8f0a8b 100644 --- a/theories/Numbers/Natural/Abstract/NAxioms.v +++ b/theories/Numbers/Natural/Abstract/NAxioms.v @@ -8,8 +8,6 @@ (* Evgeny Makarov, INRIA, 2007 *) (************************************************************************) -(*i $Id$ i*) - Require Export NZAxioms. Set Implicit Arguments. diff --git a/theories/Numbers/Natural/Abstract/NBase.v b/theories/Numbers/Natural/Abstract/NBase.v index 842f4bcf23..f26f56d0c5 100644 --- a/theories/Numbers/Natural/Abstract/NBase.v +++ b/theories/Numbers/Natural/Abstract/NBase.v @@ -8,8 +8,6 @@ (* Evgeny Makarov, INRIA, 2007 *) (************************************************************************) -(*i $Id$ i*) - Require Export Decidable. Require Export NAxioms. Require Import NZProperties. diff --git a/theories/Numbers/Natural/Abstract/NDefOps.v b/theories/Numbers/Natural/Abstract/NDefOps.v index 22eb2cb34a..2302e8d357 100644 --- a/theories/Numbers/Natural/Abstract/NDefOps.v +++ b/theories/Numbers/Natural/Abstract/NDefOps.v @@ -8,8 +8,6 @@ (* Evgeny Makarov, INRIA, 2007 *) (************************************************************************) -(*i $Id$ i*) - Require Import Bool. (* To get the orb and negb function *) Require Import RelationPairs. Require Export NStrongRec. diff --git a/theories/Numbers/Natural/Abstract/NIso.v b/theories/Numbers/Natural/Abstract/NIso.v index 47bf38cbaf..12dcd32587 100644 --- a/theories/Numbers/Natural/Abstract/NIso.v +++ b/theories/Numbers/Natural/Abstract/NIso.v @@ -8,8 +8,6 @@ (* Evgeny Makarov, INRIA, 2007 *) (************************************************************************) -(*i $Id$ i*) - Require Import NBase. Module Homomorphism (N1 N2 : NAxiomsSig). diff --git a/theories/Numbers/Natural/Abstract/NMulOrder.v b/theories/Numbers/Natural/Abstract/NMulOrder.v index a2162b137f..29d1838c2a 100644 --- a/theories/Numbers/Natural/Abstract/NMulOrder.v +++ b/theories/Numbers/Natural/Abstract/NMulOrder.v @@ -8,8 +8,6 @@ (* Evgeny Makarov, INRIA, 2007 *) (************************************************************************) -(*i $Id$ i*) - Require Export NAddOrder. Module NMulOrderPropFunct (Import N : NAxiomsSig'). diff --git a/theories/Numbers/Natural/Abstract/NOrder.v b/theories/Numbers/Natural/Abstract/NOrder.v index 090c02ecf6..9439e04f5c 100644 --- a/theories/Numbers/Natural/Abstract/NOrder.v +++ b/theories/Numbers/Natural/Abstract/NOrder.v @@ -8,8 +8,6 @@ (* Evgeny Makarov, INRIA, 2007 *) (************************************************************************) -(*i $Id$ i*) - Require Export NAdd. Module NOrderPropFunct (Import N : NAxiomsSig'). diff --git a/theories/Numbers/Natural/Abstract/NProperties.v b/theories/Numbers/Natural/Abstract/NProperties.v index 9fc9b290e5..eed7cac18d 100644 --- a/theories/Numbers/Natural/Abstract/NProperties.v +++ b/theories/Numbers/Natural/Abstract/NProperties.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - Require Export NAxioms NMaxMin. (** This functor summarizes all known facts about N. diff --git a/theories/Numbers/Natural/Abstract/NStrongRec.v b/theories/Numbers/Natural/Abstract/NStrongRec.v index cbbcdbff50..bd666bc8ba 100644 --- a/theories/Numbers/Natural/Abstract/NStrongRec.v +++ b/theories/Numbers/Natural/Abstract/NStrongRec.v @@ -8,8 +8,6 @@ (* Evgeny Makarov, INRIA, 2007 *) (************************************************************************) -(*i $Id$ i*) - (** This file defined the strong (course-of-value, well-founded) recursion and proves its properties *) diff --git a/theories/Numbers/Natural/Abstract/NSub.v b/theories/Numbers/Natural/Abstract/NSub.v index 1df032ea35..7d3117fdb5 100644 --- a/theories/Numbers/Natural/Abstract/NSub.v +++ b/theories/Numbers/Natural/Abstract/NSub.v @@ -8,8 +8,6 @@ (* Evgeny Makarov, INRIA, 2007 *) (************************************************************************) -(*i $Id$ i*) - Require Export NMulOrder. Module Type NSubPropFunct (Import N : NAxiomsSig'). diff --git a/theories/Numbers/Natural/BigN/NMake_gen.ml b/theories/Numbers/Natural/BigN/NMake_gen.ml index 5442a56263..20cb01b16b 100644 --- a/theories/Numbers/Natural/BigN/NMake_gen.ml +++ b/theories/Numbers/Natural/BigN/NMake_gen.ml @@ -8,8 +8,6 @@ (* Benjamin Gregoire, Laurent Thery, INRIA, 2007 *) (************************************************************************) -(*i $Id$ i*) - (*S NMake_gen.ml : this file generates NMake.v *) diff --git a/theories/Numbers/Natural/BigN/Nbasic.v b/theories/Numbers/Natural/BigN/Nbasic.v index 9772e6a1f0..9177b8092c 100644 --- a/theories/Numbers/Natural/BigN/Nbasic.v +++ b/theories/Numbers/Natural/BigN/Nbasic.v @@ -8,8 +8,6 @@ (* Benjamin Gregoire, Laurent Thery, INRIA, 2007 *) (************************************************************************) -(*i $Id$ i*) - Require Import ZArith. Require Import BigNumPrelude. Require Import Max. diff --git a/theories/Numbers/Natural/Binary/NBinary.v b/theories/Numbers/Natural/Binary/NBinary.v index e8651d47cb..ba592507b1 100644 --- a/theories/Numbers/Natural/Binary/NBinary.v +++ b/theories/Numbers/Natural/Binary/NBinary.v @@ -8,8 +8,6 @@ (* Evgeny Makarov, INRIA, 2007 *) (************************************************************************) -(*i $Id$ i*) - Require Import BinPos Ndiv_def. Require Export BinNat. Require Import NAxioms NProperties NDiv. diff --git a/theories/Numbers/Natural/Peano/NPeano.v b/theories/Numbers/Natural/Peano/NPeano.v index 80d434bab6..491c33666c 100644 --- a/theories/Numbers/Natural/Peano/NPeano.v +++ b/theories/Numbers/Natural/Peano/NPeano.v @@ -8,8 +8,6 @@ (* Evgeny Makarov, INRIA, 2007 *) (************************************************************************) -(*i $Id$ i*) - Require Import Peano Peano_dec Compare_dec EqNat NAxioms NProperties NDiv. (** Functions not already defined: div mod *) diff --git a/theories/Numbers/Natural/SpecViaZ/NSig.v b/theories/Numbers/Natural/SpecViaZ/NSig.v index 3f60cbf1a7..55a6302aa3 100644 --- a/theories/Numbers/Natural/SpecViaZ/NSig.v +++ b/theories/Numbers/Natural/SpecViaZ/NSig.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/Natural/SpecViaZ/NSigNAxioms.v b/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v index 49a60916aa..8cbd96c1fb 100644 --- a/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v +++ b/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - Require Import ZArith Nnat NAxioms NDiv NSig. (** * The interface [NSig.NType] implies the interface [NAxiomsSig] *) |
