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 | |
| 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')
323 files changed, 0 insertions, 644 deletions
diff --git a/theories/Arith/Arith.v b/theories/Arith/Arith.v index 18dbd27f96..0de9136fd0 100644 --- a/theories/Arith/Arith.v +++ b/theories/Arith/Arith.v @@ -6,7 +6,5 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - Require Export Arith_base. Require Export ArithRing. diff --git a/theories/Arith/Arith_base.v b/theories/Arith/Arith_base.v index 2d54f0e8d9..9395fc56c2 100644 --- a/theories/Arith/Arith_base.v +++ b/theories/Arith/Arith_base.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - Require Export Le. Require Export Lt. Require Export Plus. diff --git a/theories/Arith/Between.v b/theories/Arith/Between.v index 208c257891..b4cdb3c826 100644 --- a/theories/Arith/Between.v +++ b/theories/Arith/Between.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - Require Import Le. Require Import Lt. diff --git a/theories/Arith/Bool_nat.v b/theories/Arith/Bool_nat.v index 9fd59e103b..d94a71c9ef 100644 --- a/theories/Arith/Bool_nat.v +++ b/theories/Arith/Bool_nat.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) - Require Export Compare_dec. Require Export Peano_dec. Require Import Sumbool. diff --git a/theories/Arith/Compare.v b/theories/Arith/Compare.v index 0f2595b266..c401eb283c 100644 --- a/theories/Arith/Compare.v +++ b/theories/Arith/Compare.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - (** Equality is decidable on [nat] *) Open Local Scope nat_scope. diff --git a/theories/Arith/Compare_dec.v b/theories/Arith/Compare_dec.v index 38d1aef0e6..635b726710 100644 --- a/theories/Arith/Compare_dec.v +++ b/theories/Arith/Compare_dec.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - Require Import Le. Require Import Lt. Require Import Gt. diff --git a/theories/Arith/Div2.v b/theories/Arith/Div2.v index 999a645448..c717e9bf58 100644 --- a/theories/Arith/Div2.v +++ b/theories/Arith/Div2.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - Require Import Lt. Require Import Plus. Require Import Compare_dec. diff --git a/theories/Arith/EqNat.v b/theories/Arith/EqNat.v index 312b76e97e..7d5b36ae59 100644 --- a/theories/Arith/EqNat.v +++ b/theories/Arith/EqNat.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - (** Equality on natural numbers *) Open Local Scope nat_scope. diff --git a/theories/Arith/Euclid.v b/theories/Arith/Euclid.v index f50dcc84de..f118eb85b9 100644 --- a/theories/Arith/Euclid.v +++ b/theories/Arith/Euclid.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - Require Import Mult. Require Import Compare_dec. Require Import Wf_nat. diff --git a/theories/Arith/Even.v b/theories/Arith/Even.v index eaa1bb2d61..fa4414146e 100644 --- a/theories/Arith/Even.v +++ b/theories/Arith/Even.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - (** Here we define the predicates [even] and [odd] by mutual induction and we prove the decidability and the exclusion of those predicates. The main results about parity are proved in the module Div2. *) diff --git a/theories/Arith/Factorial.v b/theories/Arith/Factorial.v index 8c53156241..58631a987b 100644 --- a/theories/Arith/Factorial.v +++ b/theories/Arith/Factorial.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - Require Import Plus. Require Import Mult. Require Import Lt. diff --git a/theories/Arith/Gt.v b/theories/Arith/Gt.v index 70169f52a5..20aad5c055 100644 --- a/theories/Arith/Gt.v +++ b/theories/Arith/Gt.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - (** Theorems about [gt] in [nat]. [gt] is defined in [Init/Peano.v] as: << Definition gt (n m:nat) := m < n. diff --git a/theories/Arith/Le.v b/theories/Arith/Le.v index 6140eeb5a3..edf1e34d57 100644 --- a/theories/Arith/Le.v +++ b/theories/Arith/Le.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - (** Order on natural numbers. [le] is defined in [Init/Peano.v] as: << Inductive le (n:nat) : nat -> Prop := diff --git a/theories/Arith/Lt.v b/theories/Arith/Lt.v index af435e54b2..12819940d6 100644 --- a/theories/Arith/Lt.v +++ b/theories/Arith/Lt.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - (** Theorems about [lt] in nat. [lt] is defined in library [Init/Peano.v] as: << Definition lt (n m:nat) := S n <= m. diff --git a/theories/Arith/Max.v b/theories/Arith/Max.v index b94cc24855..ffce727743 100644 --- a/theories/Arith/Max.v +++ b/theories/Arith/Max.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - (** THIS FILE IS DEPRECATED. Use [NPeano.Nat] instead. *) Require Export NPeano. diff --git a/theories/Arith/Min.v b/theories/Arith/Min.v index ba03a40bd4..c980baf09a 100644 --- a/theories/Arith/Min.v +++ b/theories/Arith/Min.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - (** THIS FILE IS DEPRECATED. Use [NPeano.Nat] instead. *) Require Export NPeano. diff --git a/theories/Arith/Minus.v b/theories/Arith/Minus.v index cd6c0a29e6..490bf8e553 100644 --- a/theories/Arith/Minus.v +++ b/theories/Arith/Minus.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - (** [minus] (difference between two natural numbers) is defined in [Init/Peano.v] as: << Fixpoint minus (n m:nat) : nat := diff --git a/theories/Arith/Mult.v b/theories/Arith/Mult.v index 8346cae38b..811068daf0 100644 --- a/theories/Arith/Mult.v +++ b/theories/Arith/Mult.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - Require Export Plus. Require Export Minus. Require Export Lt. diff --git a/theories/Arith/Peano_dec.v b/theories/Arith/Peano_dec.v index 42335f98ba..d8b46c78fb 100644 --- a/theories/Arith/Peano_dec.v +++ b/theories/Arith/Peano_dec.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - Require Import Decidable. Open Local Scope nat_scope. diff --git a/theories/Arith/Plus.v b/theories/Arith/Plus.v index 9b7c626156..28613eecc6 100644 --- a/theories/Arith/Plus.v +++ b/theories/Arith/Plus.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - (** Properties of addition. [add] is defined in [Init/Peano.v] as: << Fixpoint plus (n m:nat) : nat := diff --git a/theories/Arith/Wf_nat.v b/theories/Arith/Wf_nat.v index 5bc5d2a584..c12a577f8e 100644 --- a/theories/Arith/Wf_nat.v +++ b/theories/Arith/Wf_nat.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - (** Well-founded relations and natural numbers *) Require Import Lt. diff --git a/theories/Bool/Bool.v b/theories/Bool/Bool.v index 66ab6f1c8b..a1ea2ebc8c 100644 --- a/theories/Bool/Bool.v +++ b/theories/Bool/Bool.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - (** The type [bool] is defined in the prelude as [Inductive bool : Set := true : bool | false : bool] *) diff --git a/theories/Bool/BoolEq.v b/theories/Bool/BoolEq.v index 625cbd194d..9a2e738ebf 100644 --- a/theories/Bool/BoolEq.v +++ b/theories/Bool/BoolEq.v @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) (* Cuihtlauac Alvarado - octobre 2000 *) (** Properties of a boolean equality *) diff --git a/theories/Bool/Bvector.v b/theories/Bool/Bvector.v index d9da086721..b41d65c39c 100644 --- a/theories/Bool/Bvector.v +++ b/theories/Bool/Bvector.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - (** Bit vectors. Contribution by Jean Duprat (ENS Lyon). *) Require Export Bool Sumbool. diff --git a/theories/Bool/DecBool.v b/theories/Bool/DecBool.v index 90f7ee662f..799438d89f 100644 --- a/theories/Bool/DecBool.v +++ b/theories/Bool/DecBool.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - Set Implicit Arguments. Definition ifdec (A B:Prop) (C:Type) (H:{A} + {B}) (x y:C) : C := diff --git a/theories/Bool/IfProp.v b/theories/Bool/IfProp.v index c2b5ed7932..573916ddcc 100644 --- a/theories/Bool/IfProp.v +++ b/theories/Bool/IfProp.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - Require Import Bool. Inductive IfProp (A B:Prop) : bool -> Prop := diff --git a/theories/Bool/Sumbool.v b/theories/Bool/Sumbool.v index 06ab77cfbb..a34c49175e 100644 --- a/theories/Bool/Sumbool.v +++ b/theories/Bool/Sumbool.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - (** Here are collected some results about the type sumbool (see INIT/Specif.v) [sumbool A B], which is written [{A}+{B}], is the informative disjunction "A or B", where A and B are logical propositions. diff --git a/theories/Bool/Zerob.v b/theories/Bool/Zerob.v index 5e9d4afa64..fde0530267 100644 --- a/theories/Bool/Zerob.v +++ b/theories/Bool/Zerob.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - Require Import Arith. Require Import Bool. diff --git a/theories/Classes/EquivDec.v b/theories/Classes/EquivDec.v index 0a35ef45e0..75c51a8ddb 100644 --- a/theories/Classes/EquivDec.v +++ b/theories/Classes/EquivDec.v @@ -12,8 +12,6 @@ Institution: LRI, CNRS UMR 8623 - University Paris Sud *) -(* $Id$ *) - (** Export notations. *) Require Export Coq.Classes.Equivalence. diff --git a/theories/Classes/Equivalence.v b/theories/Classes/Equivalence.v index d0f243474c..d62bd0674a 100644 --- a/theories/Classes/Equivalence.v +++ b/theories/Classes/Equivalence.v @@ -12,8 +12,6 @@ Institution: LRI, CNRS UMR 8623 - University Paris Sud *) -(* $Id$ *) - Require Import Coq.Program.Basics. Require Import Coq.Program.Tactics. diff --git a/theories/Classes/Init.v b/theories/Classes/Init.v index f6e51018a2..df288add47 100644 --- a/theories/Classes/Init.v +++ b/theories/Classes/Init.v @@ -13,8 +13,6 @@ Institution: LRI, CNRS UMR 8623 - University Paris Sud *) -(* $Id$ *) - (** Hints for the proof search: these combinators should be considered rigid. *) Require Import Coq.Program.Basics. diff --git a/theories/Classes/Morphisms.v b/theories/Classes/Morphisms.v index 4b827c2446..2421c90d06 100644 --- a/theories/Classes/Morphisms.v +++ b/theories/Classes/Morphisms.v @@ -13,8 +13,6 @@ Institution: LRI, CNRS UMR 8623 - University Paris Sud *) -(* $Id$ *) - Require Import Coq.Program.Basics. Require Import Coq.Program.Tactics. Require Import Coq.Relations.Relation_Definitions. diff --git a/theories/Classes/RelationClasses.v b/theories/Classes/RelationClasses.v index a8193ef3c8..4c39964a9a 100644 --- a/theories/Classes/RelationClasses.v +++ b/theories/Classes/RelationClasses.v @@ -15,8 +15,6 @@ Institution: LRI, CNRS UMR 8623 - University Paris Sud *) -(* $Id$ *) - Require Export Coq.Classes.Init. Require Import Coq.Program.Basics. Require Import Coq.Program.Tactics. diff --git a/theories/Classes/SetoidClass.v b/theories/Classes/SetoidClass.v index c41c576982..36fe2b9a68 100644 --- a/theories/Classes/SetoidClass.v +++ b/theories/Classes/SetoidClass.v @@ -12,8 +12,6 @@ Institution: LRI, CNRS UMR 8623 - University Paris Sud *) -(* $Id$ *) - Set Implicit Arguments. Unset Strict Implicit. diff --git a/theories/Classes/SetoidDec.v b/theories/Classes/SetoidDec.v index 33b4350f83..ab21311859 100644 --- a/theories/Classes/SetoidDec.v +++ b/theories/Classes/SetoidDec.v @@ -13,8 +13,6 @@ Institution: LRI, CNRS UMR 8623 - University Paris Sud *) -(* $Id$ *) - Set Implicit Arguments. Unset Strict Implicit. diff --git a/theories/Classes/SetoidTactics.v b/theories/Classes/SetoidTactics.v index 669be8b0ff..dbdff45f33 100644 --- a/theories/Classes/SetoidTactics.v +++ b/theories/Classes/SetoidTactics.v @@ -12,8 +12,6 @@ Institution: LRI, CNRS UMR 8623 - University Paris Sud *) -(* $Id$ *) - Require Import Coq.Classes.Morphisms Coq.Classes.Morphisms_Prop. Require Export Coq.Classes.RelationClasses Coq.Relations.Relation_Definitions. Require Import Coq.Classes.Equivalence Coq.Program.Basics. diff --git a/theories/FSets/FMapAVL.v b/theories/FSets/FMapAVL.v index c6252de9c7..e0ddbe3ab1 100644 --- a/theories/FSets/FMapAVL.v +++ b/theories/FSets/FMapAVL.v @@ -8,8 +8,6 @@ (* Finite map library. *) -(* $Id$ *) - (** * FMapAVL *) (** This module implements maps using AVL trees. diff --git a/theories/FSets/FMapFacts.v b/theories/FSets/FMapFacts.v index 4c59971cbe..fd58ec10a2 100644 --- a/theories/FSets/FMapFacts.v +++ b/theories/FSets/FMapFacts.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) -(* $Id$ *) - (** * Finite maps library *) (** This functor derives additional facts from [FMapInterface.S]. These diff --git a/theories/FSets/FMapFullAVL.v b/theories/FSets/FMapFullAVL.v index afac5af8c3..1facce2901 100644 --- a/theories/FSets/FMapFullAVL.v +++ b/theories/FSets/FMapFullAVL.v @@ -8,8 +8,6 @@ (* Finite map library. *) -(* $Id$ *) - (** * FMapFullAVL This file contains some complements to [FMapAVL]. diff --git a/theories/FSets/FMapInterface.v b/theories/FSets/FMapInterface.v index e60cca9d97..252e679306 100644 --- a/theories/FSets/FMapInterface.v +++ b/theories/FSets/FMapInterface.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) -(* $Id$ *) - (** * Finite map library *) (** This file proposes interfaces for finite maps *) diff --git a/theories/FSets/FMapList.v b/theories/FSets/FMapList.v index 56fc35d89e..f15ab222ce 100644 --- a/theories/FSets/FMapList.v +++ b/theories/FSets/FMapList.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) -(* $Id$ *) - (** * Finite map library *) (** This file proposes an implementation of the non-dependant interface diff --git a/theories/FSets/FMapPositive.v b/theories/FSets/FMapPositive.v index 56ad2ed11a..e85cc283e8 100644 --- a/theories/FSets/FMapPositive.v +++ b/theories/FSets/FMapPositive.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) -(* $Id$ *) - (** * FMapPositive : an implementation of FMapInterface for [positive] keys. *) Require Import Bool. diff --git a/theories/FSets/FMapWeakList.v b/theories/FSets/FMapWeakList.v index 38ed172b85..6c1e8ca89b 100644 --- a/theories/FSets/FMapWeakList.v +++ b/theories/FSets/FMapWeakList.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) -(* $Id$ *) - (** * Finite map library *) (** This file proposes an implementation of the non-dependant interface diff --git a/theories/FSets/FMaps.v b/theories/FSets/FMaps.v index 6b11024064..19b25d95a7 100644 --- a/theories/FSets/FMaps.v +++ b/theories/FSets/FMaps.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) -(* $Id$ *) - Require Export OrderedType OrderedTypeEx OrderedTypeAlt. Require Export DecidableType DecidableTypeEx. diff --git a/theories/FSets/FSetAVL.v b/theories/FSets/FSetAVL.v index bc6c731f62..df627a14bd 100644 --- a/theories/FSets/FSetAVL.v +++ b/theories/FSets/FSetAVL.v @@ -7,8 +7,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) -(* $Id$ *) - (** * FSetAVL : Implementation of FSetInterface via AVL trees *) (** This module implements finite sets using AVL trees. diff --git a/theories/FSets/FSetBridge.v b/theories/FSets/FSetBridge.v index 1b1bae352d..8d6ca420bb 100644 --- a/theories/FSets/FSetBridge.v +++ b/theories/FSets/FSetBridge.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) -(* $Id$ *) - (** * Finite sets library *) (** This module implements bridges (as functors) from dependent diff --git a/theories/FSets/FSetDecide.v b/theories/FSets/FSetDecide.v index 89cdc932fa..a871032322 100644 --- a/theories/FSets/FSetDecide.v +++ b/theories/FSets/FSetDecide.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) -(* $Id$ *) - (**************************************************************) (* FSetDecide.v *) (* *) diff --git a/theories/FSets/FSetEqProperties.v b/theories/FSets/FSetEqProperties.v index ec0c6a559d..755bc7dd02 100644 --- a/theories/FSets/FSetEqProperties.v +++ b/theories/FSets/FSetEqProperties.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) -(* $Id$ *) - (** * Finite sets library *) (** This module proves many properties of finite sets that diff --git a/theories/FSets/FSetFacts.v b/theories/FSets/FSetFacts.v index b750edfc0a..f473b33427 100644 --- a/theories/FSets/FSetFacts.v +++ b/theories/FSets/FSetFacts.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) -(* $Id$ *) - (** * Finite sets library *) (** This functor derives additional facts from [FSetInterface.S]. These diff --git a/theories/FSets/FSetInterface.v b/theories/FSets/FSetInterface.v index 8aede55272..a232638902 100644 --- a/theories/FSets/FSetInterface.v +++ b/theories/FSets/FSetInterface.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) -(* $Id$ *) - (** * Finite set library *) (** Set interfaces, inspired by the one of Ocaml. When compared with diff --git a/theories/FSets/FSetList.v b/theories/FSets/FSetList.v index f83259c447..1f36306c34 100644 --- a/theories/FSets/FSetList.v +++ b/theories/FSets/FSetList.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) -(* $Id$ *) - (** * Finite sets library *) (** This file proposes an implementation of the non-dependant diff --git a/theories/FSets/FSetProperties.v b/theories/FSets/FSetProperties.v index 84c26dacdb..80da1c5d81 100644 --- a/theories/FSets/FSetProperties.v +++ b/theories/FSets/FSetProperties.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) -(* $Id$ *) - (** * Finite sets library *) (** This functor derives additional properties from [FSetInterface.S]. diff --git a/theories/FSets/FSetToFiniteSet.v b/theories/FSets/FSetToFiniteSet.v index 01138270e2..3ac5d9e4ae 100644 --- a/theories/FSets/FSetToFiniteSet.v +++ b/theories/FSets/FSetToFiniteSet.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) -(* $Id$ *) - (** * Finite sets library : conversion to old [Finite_sets] *) Require Import Ensembles Finite_sets. diff --git a/theories/FSets/FSetWeakList.v b/theories/FSets/FSetWeakList.v index 711cbd9a68..2ea32e97cb 100644 --- a/theories/FSets/FSetWeakList.v +++ b/theories/FSets/FSetWeakList.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) -(* $Id$ *) - (** * Finite sets library *) (** This file proposes an implementation of the non-dependant diff --git a/theories/FSets/FSets.v b/theories/FSets/FSets.v index eaa8f40343..9a72941195 100644 --- a/theories/FSets/FSets.v +++ b/theories/FSets/FSets.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) -(* $Id$ *) - Require Export OrderedType. Require Export OrderedTypeEx. Require Export OrderedTypeAlt. diff --git a/theories/Init/Datatypes.v b/theories/Init/Datatypes.v index 092fce996f..782ff6ca95 100644 --- a/theories/Init/Datatypes.v +++ b/theories/Init/Datatypes.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - Set Implicit Arguments. Require Import Notations. diff --git a/theories/Init/Logic.v b/theories/Init/Logic.v index 4fca1d1dbb..14832e0b72 100644 --- a/theories/Init/Logic.v +++ b/theories/Init/Logic.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - Set Implicit Arguments. Require Import Notations. diff --git a/theories/Init/Logic_Type.v b/theories/Init/Logic_Type.v index 1333f3545e..ff6a18e147 100644 --- a/theories/Init/Logic_Type.v +++ b/theories/Init/Logic_Type.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - (** This module defines type constructors for types in [Type] ([Datatypes.v] and [Logic.v] defined them for types in [Set]) *) diff --git a/theories/Init/Notations.v b/theories/Init/Notations.v index 0c628298dc..9bf921b225 100644 --- a/theories/Init/Notations.v +++ b/theories/Init/Notations.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - (** These are the notations whose level and associativity are imposed by Coq *) (** Notations for propositional connectives *) diff --git a/theories/Init/Peano.v b/theories/Init/Peano.v index 8779f2b452..045210d0ae 100644 --- a/theories/Init/Peano.v +++ b/theories/Init/Peano.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - (** The type [nat] of Peano natural numbers (built from [O] and [S]) is defined in [Datatypes.v] *) diff --git a/theories/Init/Prelude.v b/theories/Init/Prelude.v index 45b949716c..c8d809fd48 100644 --- a/theories/Init/Prelude.v +++ b/theories/Init/Prelude.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - Require Export Notations. Require Export Logic. Require Export Datatypes. diff --git a/theories/Init/Specif.v b/theories/Init/Specif.v index 7141f26cb5..6ff8202995 100644 --- a/theories/Init/Specif.v +++ b/theories/Init/Specif.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - (** Basic specifications : sets that may contain logical information *) Set Implicit Arguments. diff --git a/theories/Init/Tactics.v b/theories/Init/Tactics.v index 6ccf8a0228..66f90e18f1 100644 --- a/theories/Init/Tactics.v +++ b/theories/Init/Tactics.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - Require Import Notations. Require Import Logic. Require Import Specif. diff --git a/theories/Init/Wf.v b/theories/Init/Wf.v index 3209860f34..0a1a0f9b8c 100644 --- a/theories/Init/Wf.v +++ b/theories/Init/Wf.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - (** * This module proves the validity of - well-founded recursion (also known as course of values) - well-founded induction diff --git a/theories/Lists/List.v b/theories/Lists/List.v index 766456fff7..d1e3f90b32 100644 --- a/theories/Lists/List.v +++ b/theories/Lists/List.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - Require Import Le Gt Minus Bool. Set Implicit Arguments. diff --git a/theories/Lists/ListSet.v b/theories/Lists/ListSet.v index e6c3a435be..0ed3bbbb75 100644 --- a/theories/Lists/ListSet.v +++ b/theories/Lists/ListSet.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - (** A Library for finite sets, implemented as lists *) (** List is loaded, but not exported. diff --git a/theories/Lists/ListTactics.v b/theories/Lists/ListTactics.v index 0a21a9e277..3a743dd47d 100644 --- a/theories/Lists/ListTactics.v +++ b/theories/Lists/ListTactics.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - Require Import BinPos. Require Import List. diff --git a/theories/Lists/SetoidList.v b/theories/Lists/SetoidList.v index d42e71e556..88ccdb1261 100644 --- a/theories/Lists/SetoidList.v +++ b/theories/Lists/SetoidList.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) -(* $Id$ *) - Require Export List. Require Export Sorting. Require Export Setoid Basics Morphisms. diff --git a/theories/Lists/Streams.v b/theories/Lists/Streams.v index 3fa053b7fc..39a2968f77 100644 --- a/theories/Lists/Streams.v +++ b/theories/Lists/Streams.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - Set Implicit Arguments. (** Streams *) diff --git a/theories/Lists/TheoryList.v b/theories/Lists/TheoryList.v index 7ed9c519b6..2d75f065f8 100644 --- a/theories/Lists/TheoryList.v +++ b/theories/Lists/TheoryList.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - (** Some programs and results about lists following CAML Manual *) Require Export List. diff --git a/theories/Logic/Berardi.v b/theories/Logic/Berardi.v index 5b2f5063b9..b32456a9ed 100644 --- a/theories/Logic/Berardi.v +++ b/theories/Logic/Berardi.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - (** This file formalizes Berardi's paradox which says that in the calculus of constructions, excluded middle (EM) and axiom of choice (AC) imply proof irrelevance (PI). diff --git a/theories/Logic/ChoiceFacts.v b/theories/Logic/ChoiceFacts.v index b2c4a049d2..903081ce6a 100644 --- a/theories/Logic/ChoiceFacts.v +++ b/theories/Logic/ChoiceFacts.v @@ -7,8 +7,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: ChoiceFacts.v 12363 2009-09-28 15:04:07Z letouzey $ i*) - (** Some facts and definitions concerning choice and description in intuitionistic logic. diff --git a/theories/Logic/Classical.v b/theories/Logic/Classical.v index 1c2b97ce76..4a01f3fae5 100644 --- a/theories/Logic/Classical.v +++ b/theories/Logic/Classical.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - (** Classical Logic *) Require Export Classical_Prop. diff --git a/theories/Logic/ClassicalChoice.v b/theories/Logic/ClassicalChoice.v index b0301994b6..92e48e6a95 100644 --- a/theories/Logic/ClassicalChoice.v +++ b/theories/Logic/ClassicalChoice.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - (** This file provides classical logic and functional choice; this especially provides both indefinite descriptions and choice functions but this is weaker than providing epsilon operator and classical logic diff --git a/theories/Logic/ClassicalDescription.v b/theories/Logic/ClassicalDescription.v index 2b9df6d977..a5d1babaa4 100644 --- a/theories/Logic/ClassicalDescription.v +++ b/theories/Logic/ClassicalDescription.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - (** This file provides classical logic and definite description, which is equivalent to providing classical logic and Church's iota operator *) diff --git a/theories/Logic/ClassicalEpsilon.v b/theories/Logic/ClassicalEpsilon.v index cee55dc815..7de6ddab6d 100644 --- a/theories/Logic/ClassicalEpsilon.v +++ b/theories/Logic/ClassicalEpsilon.v @@ -7,8 +7,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - (** This file provides classical logic and indefinite description under the form of Hilbert's epsilon operator *) diff --git a/theories/Logic/ClassicalFacts.v b/theories/Logic/ClassicalFacts.v index b22a3a8743..a271c05bca 100644 --- a/theories/Logic/ClassicalFacts.v +++ b/theories/Logic/ClassicalFacts.v @@ -7,8 +7,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - (** Some facts and definitions about classical logic Table of contents: diff --git a/theories/Logic/ClassicalUniqueChoice.v b/theories/Logic/ClassicalUniqueChoice.v index 4a7bd2ccc6..67b853be94 100644 --- a/theories/Logic/ClassicalUniqueChoice.v +++ b/theories/Logic/ClassicalUniqueChoice.v @@ -7,8 +7,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - (** This file provides classical logic and unique choice; this is weaker than providing iota operator and classical logic as the definite descriptions provided by the axiom of unique choice can diff --git a/theories/Logic/Classical_Pred_Set.v b/theories/Logic/Classical_Pred_Set.v index 0b0c329bec..afbb5e6dfc 100644 --- a/theories/Logic/Classical_Pred_Set.v +++ b/theories/Logic/Classical_Pred_Set.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - (** This file is obsolete, use Classical_Pred_Type.v via Classical.v instead *) diff --git a/theories/Logic/Classical_Pred_Type.v b/theories/Logic/Classical_Pred_Type.v index b30308af5e..45c487cf7b 100644 --- a/theories/Logic/Classical_Pred_Type.v +++ b/theories/Logic/Classical_Pred_Type.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - (** Classical Predicate Logic on Type *) Require Import Classical_Prop. diff --git a/theories/Logic/Classical_Prop.v b/theories/Logic/Classical_Prop.v index df732959f3..ee6dd96f2a 100644 --- a/theories/Logic/Classical_Prop.v +++ b/theories/Logic/Classical_Prop.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - (** Classical Propositional Logic *) Require Import ClassicalFacts. diff --git a/theories/Logic/Classical_Type.v b/theories/Logic/Classical_Type.v index 3b91afd02f..b3053fa1d1 100644 --- a/theories/Logic/Classical_Type.v +++ b/theories/Logic/Classical_Type.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - (** This file is obsolete, use Classical.v instead *) (** Classical Logic for Type *) diff --git a/theories/Logic/ConstructiveEpsilon.v b/theories/Logic/ConstructiveEpsilon.v index 6d22b1a9ed..8077cabf76 100644 --- a/theories/Logic/ConstructiveEpsilon.v +++ b/theories/Logic/ConstructiveEpsilon.v @@ -7,8 +7,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - (** This module proves the constructive description schema, which infers the sigma-existence (i.e., [Set]-existence) of a witness to a predicate from the regular existence (i.e., [Prop]-existence). One diff --git a/theories/Logic/Decidable.v b/theories/Logic/Decidable.v index c6d32d9bef..75441584d0 100644 --- a/theories/Logic/Decidable.v +++ b/theories/Logic/Decidable.v @@ -5,8 +5,6 @@ (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - (** Properties of decidable propositions *) Definition decidable (P:Prop) := P \/ ~ P. diff --git a/theories/Logic/Description.v b/theories/Logic/Description.v index a8a56ae740..dd1d56b31f 100644 --- a/theories/Logic/Description.v +++ b/theories/Logic/Description.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - (** This file provides a constructive form of definite description; it allows to build functions from the proof of their existence in any context; this is weaker than Church's iota operator *) diff --git a/theories/Logic/Diaconescu.v b/theories/Logic/Diaconescu.v index 18f3181b66..b513bdf731 100644 --- a/theories/Logic/Diaconescu.v +++ b/theories/Logic/Diaconescu.v @@ -7,8 +7,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - (** Diaconescu showed that the Axiom of Choice entails Excluded-Middle in topoi [Diaconescu75]. Lacas and Werner adapted the proof to show that the axiom of choice in equivalence classes entails diff --git a/theories/Logic/Epsilon.v b/theories/Logic/Epsilon.v index d433be944b..7de0aa7fcd 100644 --- a/theories/Logic/Epsilon.v +++ b/theories/Logic/Epsilon.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - (** This file provides indefinite description under the form of Hilbert's epsilon operator; it does not assume classical logic. *) diff --git a/theories/Logic/Eqdep.v b/theories/Logic/Eqdep.v index 5c6b4e89f3..14ab70b67c 100644 --- a/theories/Logic/Eqdep.v +++ b/theories/Logic/Eqdep.v @@ -7,8 +7,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - (** This file axiomatizes the invariance by substitution of reflexive equality proofs [[Streicher93]] and exports its consequences, such as the injectivity of the projection of the dependent pair. diff --git a/theories/Logic/EqdepFacts.v b/theories/Logic/EqdepFacts.v index 4689fb46c0..9c20905c76 100644 --- a/theories/Logic/EqdepFacts.v +++ b/theories/Logic/EqdepFacts.v @@ -7,8 +7,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - (** This file defines dependent equality and shows its equivalence with equality on dependent pairs (inhabiting sigma-types). It derives the consequence of axiomatizing the invariance by substitution of diff --git a/theories/Logic/Eqdep_dec.v b/theories/Logic/Eqdep_dec.v index c7cb9b0d45..d4d05fe1a7 100644 --- a/theories/Logic/Eqdep_dec.v +++ b/theories/Logic/Eqdep_dec.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - (** We prove that there is only one proof of [x=x], i.e [refl_equal x]. This holds if the equality upon the set of [x] is decidable. A corollary of this theorem is the equality of the right projections diff --git a/theories/Logic/FunctionalExtensionality.v b/theories/Logic/FunctionalExtensionality.v index bf29c63dda..5d6a4f7d64 100644 --- a/theories/Logic/FunctionalExtensionality.v +++ b/theories/Logic/FunctionalExtensionality.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - (** This module states the axiom of (dependent) functional extensionality and (dependent) eta-expansion. It introduces a tactic [extensionality] to apply the axiom of extensionality to an equality goal. *) diff --git a/theories/Logic/IndefiniteDescription.v b/theories/Logic/IndefiniteDescription.v index 3651c1b2fa..94922525b0 100644 --- a/theories/Logic/IndefiniteDescription.v +++ b/theories/Logic/IndefiniteDescription.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - (** This file provides a constructive form of indefinite description that allows to build choice functions; this is weaker than Hilbert's epsilon operator (which implies weakly classical properties) but diff --git a/theories/Logic/JMeq.v b/theories/Logic/JMeq.v index fc4555a4ad..f17e403ed9 100644 --- a/theories/Logic/JMeq.v +++ b/theories/Logic/JMeq.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - (** John Major's Equality as proposed by Conor McBride Reference: diff --git a/theories/Logic/RelationalChoice.v b/theories/Logic/RelationalChoice.v index 49fa122248..9313e1073b 100644 --- a/theories/Logic/RelationalChoice.v +++ b/theories/Logic/RelationalChoice.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - (** This file axiomatizes the relational form of the axiom of choice *) Axiom relational_choice : diff --git a/theories/MSets/MSetAVL.v b/theories/MSets/MSetAVL.v index f79f8d0b26..0d24e0339e 100644 --- a/theories/MSets/MSetAVL.v +++ b/theories/MSets/MSetAVL.v @@ -7,8 +7,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) -(* $Id$ *) - (** * MSetAVL : Implementation of MSetInterface via AVL trees *) (** This module implements finite sets using AVL trees. diff --git a/theories/MSets/MSetDecide.v b/theories/MSets/MSetDecide.v index 884ed42353..1161739ed9 100644 --- a/theories/MSets/MSetDecide.v +++ b/theories/MSets/MSetDecide.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) -(* $Id$ *) - (**************************************************************) (* MSetDecide.v *) (* *) diff --git a/theories/MSets/MSetEqProperties.v b/theories/MSets/MSetEqProperties.v index fe6c3c79c2..2e7da404e8 100644 --- a/theories/MSets/MSetEqProperties.v +++ b/theories/MSets/MSetEqProperties.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) -(* $Id$ *) - (** * Finite sets library *) (** This module proves many properties of finite sets that diff --git a/theories/MSets/MSetFacts.v b/theories/MSets/MSetFacts.v index 84f6a17055..b61bf3fe79 100644 --- a/theories/MSets/MSetFacts.v +++ b/theories/MSets/MSetFacts.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) -(* $Id$ *) - (** * Finite sets library *) (** This functor derives additional facts from [MSetInterface.S]. These diff --git a/theories/MSets/MSetInterface.v b/theories/MSets/MSetInterface.v index 10776a5909..7dc3c96a86 100644 --- a/theories/MSets/MSetInterface.v +++ b/theories/MSets/MSetInterface.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) -(* $Id$ *) - (** * Finite set library *) (** Set interfaces, inspired by the one of Ocaml. When compared with diff --git a/theories/MSets/MSetList.v b/theories/MSets/MSetList.v index 0414e6eda9..b73af8f1ab 100644 --- a/theories/MSets/MSetList.v +++ b/theories/MSets/MSetList.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) -(* $Id$ *) - (** * Finite sets library *) (** This file proposes an implementation of the non-dependant diff --git a/theories/MSets/MSetProperties.v b/theories/MSets/MSetProperties.v index a9ba0a823b..14fe097a93 100644 --- a/theories/MSets/MSetProperties.v +++ b/theories/MSets/MSetProperties.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) -(* $Id$ *) - (** * Finite sets library *) (** This functor derives additional properties from [MSetInterface.S]. diff --git a/theories/MSets/MSetToFiniteSet.v b/theories/MSets/MSetToFiniteSet.v index f0b964cf2d..e8087bc572 100644 --- a/theories/MSets/MSetToFiniteSet.v +++ b/theories/MSets/MSetToFiniteSet.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) -(* $Id$ *) - (** * Finite sets library : conversion to old [Finite_sets] *) Require Import Ensembles Finite_sets. diff --git a/theories/MSets/MSetWeakList.v b/theories/MSets/MSetWeakList.v index 6b9c170790..8239ecef8b 100644 --- a/theories/MSets/MSetWeakList.v +++ b/theories/MSets/MSetWeakList.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) -(* $Id$ *) - (** * Finite sets library *) (** This file proposes an implementation of the non-dependant diff --git a/theories/MSets/MSets.v b/theories/MSets/MSets.v index 558b09562d..a4b9efc3bc 100644 --- a/theories/MSets/MSets.v +++ b/theories/MSets/MSets.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) -(* $Id$ *) - Require Export Orders. Require Export OrdersEx. Require Export OrdersAlt. diff --git a/theories/NArith/BinNat.v b/theories/NArith/BinNat.v index b289380fdf..6b668df609 100644 --- a/theories/NArith/BinNat.v +++ b/theories/NArith/BinNat.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - Require Import BinPos. Unset Boxed Definitions. diff --git a/theories/NArith/BinPos.v b/theories/NArith/BinPos.v index a5f99cc66c..a7b2336c8c 100644 --- a/theories/NArith/BinPos.v +++ b/theories/NArith/BinPos.v @@ -7,8 +7,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - Unset Boxed Definitions. Declare ML Module "z_syntax_plugin". diff --git a/theories/NArith/NArith.v b/theories/NArith/NArith.v index 009e64fd0c..7282fc758c 100644 --- a/theories/NArith/NArith.v +++ b/theories/NArith/NArith.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) - (** Library for binary natural numbers *) Require Export BinPos. diff --git a/theories/NArith/Ndec.v b/theories/NArith/Ndec.v index 9540aace7f..c217ada115 100644 --- a/theories/NArith/Ndec.v +++ b/theories/NArith/Ndec.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - Require Import Bool. Require Import Sumbool. Require Import Arith. diff --git a/theories/NArith/Ndigits.v b/theories/NArith/Ndigits.v index b699b74287..a79cfac3d8 100644 --- a/theories/NArith/Ndigits.v +++ b/theories/NArith/Ndigits.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - Require Import Bool Setoid Bvector BinPos BinNat. (** Operation over bits of a [N] number. *) diff --git a/theories/NArith/Ndist.v b/theories/NArith/Ndist.v index 92559ff674..dc37fa6c2a 100644 --- a/theories/NArith/Ndist.v +++ b/theories/NArith/Ndist.v @@ -5,8 +5,6 @@ (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - Require Import Arith. Require Import Min. Require Import BinPos. diff --git a/theories/NArith/Nnat.v b/theories/NArith/Nnat.v index 0016d035fc..feabd3b16c 100644 --- a/theories/NArith/Nnat.v +++ b/theories/NArith/Nnat.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - Require Import Arith_base. Require Import Compare_dec. Require Import Sumbool. diff --git a/theories/NArith/Pnat.v b/theories/NArith/Pnat.v index 0891dea21e..fea12a1d4d 100644 --- a/theories/NArith/Pnat.v +++ b/theories/NArith/Pnat.v @@ -7,8 +7,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - Require Import BinPos. (**********************************************************************) diff --git a/theories/Numbers/BigNumPrelude.v b/theories/Numbers/BigNumPrelude.v index 08da684441..f11fb67b1a 100644 --- a/theories/Numbers/BigNumPrelude.v +++ b/theories/Numbers/BigNumPrelude.v @@ -8,8 +8,6 @@ (* Benjamin Gregoire, Laurent Thery, INRIA, 2007 *) (************************************************************************) -(*i $Id$ i*) - (** * BigNumPrelude *) (** Auxillary functions & theorems used for arbitrary precision efficient diff --git a/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v b/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v index af30b0175b..0403722cb3 100644 --- a/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v +++ b/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v @@ -8,8 +8,6 @@ (* Benjamin Gregoire, Laurent Thery, INRIA, 2007 *) (************************************************************************) -(* $Id$ *) - (** * Signature and specification of a bounded integer structure *) (** This file specifies how to represent [Z/nZ] when [n=2^d], diff --git a/theories/Numbers/Cyclic/Abstract/NZCyclic.v b/theories/Numbers/Cyclic/Abstract/NZCyclic.v index b68e89560e..0796d9f49b 100644 --- a/theories/Numbers/Cyclic/Abstract/NZCyclic.v +++ b/theories/Numbers/Cyclic/Abstract/NZCyclic.v @@ -8,8 +8,6 @@ (* Evgeny Makarov, INRIA, 2007 *) (************************************************************************) -(*i $Id$ i*) - Require Export NZAxioms. Require Import BigNumPrelude. Require Import DoubleType. diff --git a/theories/Numbers/Cyclic/DoubleCyclic/DoubleAdd.v b/theories/Numbers/Cyclic/DoubleCyclic/DoubleAdd.v index aa798e1c7f..81b2c9403f 100644 --- a/theories/Numbers/Cyclic/DoubleCyclic/DoubleAdd.v +++ b/theories/Numbers/Cyclic/DoubleCyclic/DoubleAdd.v @@ -8,8 +8,6 @@ (* Benjamin Gregoire, Laurent Thery, INRIA, 2007 *) (************************************************************************) -(*i $Id$ i*) - Set Implicit Arguments. Require Import ZArith. diff --git a/theories/Numbers/Cyclic/DoubleCyclic/DoubleBase.v b/theories/Numbers/Cyclic/DoubleCyclic/DoubleBase.v index 23c62740c8..bf18c1753d 100644 --- a/theories/Numbers/Cyclic/DoubleCyclic/DoubleBase.v +++ b/theories/Numbers/Cyclic/DoubleCyclic/DoubleBase.v @@ -8,8 +8,6 @@ (* Benjamin Gregoire, Laurent Thery, INRIA, 2007 *) (************************************************************************) -(*i $Id$ i*) - Set Implicit Arguments. Require Import ZArith. diff --git a/theories/Numbers/Cyclic/DoubleCyclic/DoubleCyclic.v b/theories/Numbers/Cyclic/DoubleCyclic/DoubleCyclic.v index 49a4f950a8..a640aaf7f9 100644 --- a/theories/Numbers/Cyclic/DoubleCyclic/DoubleCyclic.v +++ b/theories/Numbers/Cyclic/DoubleCyclic/DoubleCyclic.v @@ -8,8 +8,6 @@ (* Benjamin Gregoire, Laurent Thery, INRIA, 2007 *) (************************************************************************) -(*i $Id$ i*) - Set Implicit Arguments. Require Import ZArith. diff --git a/theories/Numbers/Cyclic/DoubleCyclic/DoubleDiv.v b/theories/Numbers/Cyclic/DoubleCyclic/DoubleDiv.v index 1ce1e81b0c..ae806dd5e4 100644 --- a/theories/Numbers/Cyclic/DoubleCyclic/DoubleDiv.v +++ b/theories/Numbers/Cyclic/DoubleCyclic/DoubleDiv.v @@ -8,8 +8,6 @@ (* Benjamin Gregoire, Laurent Thery, INRIA, 2007 *) (************************************************************************) -(*i $Id$ i*) - Set Implicit Arguments. Require Import ZArith. diff --git a/theories/Numbers/Cyclic/DoubleCyclic/DoubleDivn1.v b/theories/Numbers/Cyclic/DoubleCyclic/DoubleDivn1.v index 136f96c043..1c4247231f 100644 --- a/theories/Numbers/Cyclic/DoubleCyclic/DoubleDivn1.v +++ b/theories/Numbers/Cyclic/DoubleCyclic/DoubleDivn1.v @@ -8,8 +8,6 @@ (* Benjamin Gregoire, Laurent Thery, INRIA, 2007 *) (************************************************************************) -(*i $Id$ i*) - Set Implicit Arguments. Require Import ZArith. diff --git a/theories/Numbers/Cyclic/DoubleCyclic/DoubleLift.v b/theories/Numbers/Cyclic/DoubleCyclic/DoubleLift.v index 3405b6f4d6..1395caa338 100644 --- a/theories/Numbers/Cyclic/DoubleCyclic/DoubleLift.v +++ b/theories/Numbers/Cyclic/DoubleCyclic/DoubleLift.v @@ -8,8 +8,6 @@ (* Benjamin Gregoire, Laurent Thery, INRIA, 2007 *) (************************************************************************) -(*i $Id$ i*) - Set Implicit Arguments. Require Import ZArith. diff --git a/theories/Numbers/Cyclic/DoubleCyclic/DoubleMul.v b/theories/Numbers/Cyclic/DoubleCyclic/DoubleMul.v index 6a2a344490..8b978172c0 100644 --- a/theories/Numbers/Cyclic/DoubleCyclic/DoubleMul.v +++ b/theories/Numbers/Cyclic/DoubleCyclic/DoubleMul.v @@ -8,8 +8,6 @@ (* Benjamin Gregoire, Laurent Thery, INRIA, 2007 *) (************************************************************************) -(*i $Id$ i*) - Set Implicit Arguments. Require Import ZArith. diff --git a/theories/Numbers/Cyclic/DoubleCyclic/DoubleSqrt.v b/theories/Numbers/Cyclic/DoubleCyclic/DoubleSqrt.v index e2c6232013..81df55bd44 100644 --- a/theories/Numbers/Cyclic/DoubleCyclic/DoubleSqrt.v +++ b/theories/Numbers/Cyclic/DoubleCyclic/DoubleSqrt.v @@ -8,8 +8,6 @@ (* Benjamin Gregoire, Laurent Thery, INRIA, 2007 *) (************************************************************************) -(*i $Id$ i*) - Set Implicit Arguments. Require Import ZArith. diff --git a/theories/Numbers/Cyclic/DoubleCyclic/DoubleSub.v b/theories/Numbers/Cyclic/DoubleCyclic/DoubleSub.v index a7e556713a..a5610fe783 100644 --- a/theories/Numbers/Cyclic/DoubleCyclic/DoubleSub.v +++ b/theories/Numbers/Cyclic/DoubleCyclic/DoubleSub.v @@ -8,8 +8,6 @@ (* Benjamin Gregoire, Laurent Thery, INRIA, 2007 *) (************************************************************************) -(*i $Id$ i*) - Set Implicit Arguments. Require Import ZArith. diff --git a/theories/Numbers/Cyclic/DoubleCyclic/DoubleType.v b/theories/Numbers/Cyclic/DoubleCyclic/DoubleType.v index 88cbb484fc..da75219a5b 100644 --- a/theories/Numbers/Cyclic/DoubleCyclic/DoubleType.v +++ b/theories/Numbers/Cyclic/DoubleCyclic/DoubleType.v @@ -8,8 +8,6 @@ (* Benjamin Gregoire, Laurent Thery, INRIA, 2007 *) (************************************************************************) -(*i $Id$ i*) - Set Implicit Arguments. Require Import ZArith. diff --git a/theories/Numbers/Cyclic/Int31/Cyclic31.v b/theories/Numbers/Cyclic/Int31/Cyclic31.v index e2e5b563f2..ca73a9f005 100644 --- a/theories/Numbers/Cyclic/Int31/Cyclic31.v +++ b/theories/Numbers/Cyclic/Int31/Cyclic31.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - (** * Int31 numbers defines indeed a cyclic structure : Z/(2^31)Z *) (** diff --git a/theories/Numbers/Cyclic/Int31/Int31.v b/theories/Numbers/Cyclic/Int31/Int31.v index cc224254f8..9b4c25e2c2 100644 --- a/theories/Numbers/Cyclic/Int31/Int31.v +++ b/theories/Numbers/Cyclic/Int31/Int31.v @@ -8,8 +8,6 @@ (* Benjamin Gregoire, Laurent Thery, INRIA, 2007 *) (************************************************************************) -(*i $Id$ i*) - Require Import NaryFunctions. Require Import Wf_nat. Require Export ZArith. diff --git a/theories/Numbers/Cyclic/Int31/Ring31.v b/theories/Numbers/Cyclic/Int31/Ring31.v index a9c499fb95..01002656df 100644 --- a/theories/Numbers/Cyclic/Int31/Ring31.v +++ b/theories/Numbers/Cyclic/Int31/Ring31.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - (** * Int31 numbers defines Z/(2^31)Z, and can hence be equipped with a ring structure and a ring tactic *) diff --git a/theories/Numbers/Cyclic/ZModulo/ZModulo.v b/theories/Numbers/Cyclic/ZModulo/ZModulo.v index da0be5e2ab..a2ee248ab0 100644 --- a/theories/Numbers/Cyclic/ZModulo/ZModulo.v +++ b/theories/Numbers/Cyclic/ZModulo/ZModulo.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) - (** * Type [Z] viewed modulo a particular constant corresponds to [Z/nZ] as defined abstractly in CyclicAxioms. *) 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] diff --git a/theories/Numbers/NaryFunctions.v b/theories/Numbers/NaryFunctions.v index 417463ebac..121b33b00e 100644 --- a/theories/Numbers/NaryFunctions.v +++ b/theories/Numbers/NaryFunctions.v @@ -8,8 +8,6 @@ (* Pierre Letouzey, Jerome Vouillon, PPS, Paris 7, 2008 *) (************************************************************************) -(*i $Id$ i*) - Local Open Scope type_scope. Require Import List. diff --git a/theories/Numbers/NatInt/NZAdd.v b/theories/Numbers/NatInt/NZAdd.v index 9535cfdb4a..37a174c48b 100644 --- a/theories/Numbers/NatInt/NZAdd.v +++ b/theories/Numbers/NatInt/NZAdd.v @@ -8,8 +8,6 @@ (* Evgeny Makarov, INRIA, 2007 *) (************************************************************************) -(*i $Id$ i*) - Require Import NZAxioms NZBase. Module Type NZAddPropSig diff --git a/theories/Numbers/NatInt/NZAddOrder.v b/theories/Numbers/NatInt/NZAddOrder.v index 97c122029f..66e9c6ceb7 100644 --- a/theories/Numbers/NatInt/NZAddOrder.v +++ b/theories/Numbers/NatInt/NZAddOrder.v @@ -8,8 +8,6 @@ (* Evgeny Makarov, INRIA, 2007 *) (************************************************************************) -(*i $Id$ i*) - Require Import NZAxioms NZBase NZMul NZOrder. Module Type NZAddOrderPropSig (Import NZ : NZOrdAxiomsSig'). diff --git a/theories/Numbers/NatInt/NZAxioms.v b/theories/Numbers/NatInt/NZAxioms.v index ee7ee159f4..7cfa62eab1 100644 --- a/theories/Numbers/NatInt/NZAxioms.v +++ b/theories/Numbers/NatInt/NZAxioms.v @@ -8,8 +8,6 @@ (** Initial Author : Evgeny Makarov, INRIA, 2007 *) -(*i $Id$ i*) - Require Export Equalities Orders NumPrelude GenericMinMax. (** Axiomatization of a domain with zero, successor, predecessor, diff --git a/theories/Numbers/NatInt/NZBase.v b/theories/Numbers/NatInt/NZBase.v index 18e3b9b921..9f587a1d08 100644 --- a/theories/Numbers/NatInt/NZBase.v +++ b/theories/Numbers/NatInt/NZBase.v @@ -8,8 +8,6 @@ (* Evgeny Makarov, INRIA, 2007 *) (************************************************************************) -(*i $Id$ i*) - Require Import NZAxioms. Module Type NZBasePropSig (Import NZ : NZDomainSig'). diff --git a/theories/Numbers/NatInt/NZDomain.v b/theories/Numbers/NatInt/NZDomain.v index eb06cae03c..7afbee4a42 100644 --- a/theories/Numbers/NatInt/NZDomain.v +++ b/theories/Numbers/NatInt/NZDomain.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - Require Export NumPrelude NZAxioms. Require Import NZBase NZOrder NZAddOrder Plus Minus. diff --git a/theories/Numbers/NatInt/NZMul.v b/theories/Numbers/NatInt/NZMul.v index 296bd095f9..c97aa9f3ae 100644 --- a/theories/Numbers/NatInt/NZMul.v +++ b/theories/Numbers/NatInt/NZMul.v @@ -8,8 +8,6 @@ (* Evgeny Makarov, INRIA, 2007 *) (************************************************************************) -(*i $Id$ i*) - Require Import NZAxioms NZBase NZAdd. Module Type NZMulPropSig diff --git a/theories/Numbers/NatInt/NZMulOrder.v b/theories/Numbers/NatInt/NZMulOrder.v index 7b64a69836..acc43fc179 100644 --- a/theories/Numbers/NatInt/NZMulOrder.v +++ b/theories/Numbers/NatInt/NZMulOrder.v @@ -8,8 +8,6 @@ (* Evgeny Makarov, INRIA, 2007 *) (************************************************************************) -(*i $Id$ i*) - Require Import NZAxioms. Require Import NZAddOrder. diff --git a/theories/Numbers/NatInt/NZOrder.v b/theories/Numbers/NatInt/NZOrder.v index 14fa0bfde1..bfbcc2c65c 100644 --- a/theories/Numbers/NatInt/NZOrder.v +++ b/theories/Numbers/NatInt/NZOrder.v @@ -8,8 +8,6 @@ (* Evgeny Makarov, INRIA, 2007 *) (************************************************************************) -(*i $Id$ i*) - Require Import NZAxioms NZBase Decidable OrdersTac. Module Type NZOrderPropSig diff --git a/theories/Numbers/NatInt/NZProperties.v b/theories/Numbers/NatInt/NZProperties.v index 125b4f62c1..cc7bfe031f 100644 --- a/theories/Numbers/NatInt/NZProperties.v +++ b/theories/Numbers/NatInt/NZProperties.v @@ -8,8 +8,6 @@ (* Evgeny Makarov, INRIA, 2007 *) (************************************************************************) -(*i $Id$ i*) - Require Export NZAxioms NZMulOrder. (** This functor summarizes all known facts about NZ. 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] *) diff --git a/theories/Numbers/NumPrelude.v b/theories/Numbers/NumPrelude.v index 32860cd31e..5022c9ae69 100644 --- a/theories/Numbers/NumPrelude.v +++ b/theories/Numbers/NumPrelude.v @@ -8,8 +8,6 @@ (* Evgeny Makarov, INRIA, 2007 *) (************************************************************************) -(*i $Id$ i*) - Require Export Setoid Morphisms. Set Implicit Arguments. diff --git a/theories/Numbers/Rational/SpecViaQ/QSig.v b/theories/Numbers/Rational/SpecViaQ/QSig.v index 10d0189a32..6466fc5118 100644 --- a/theories/Numbers/Rational/SpecViaQ/QSig.v +++ b/theories/Numbers/Rational/SpecViaQ/QSig.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - Require Import QArith Qpower Qminmax Orders RelationPairs GenericMinMax. Open Scope Q_scope. diff --git a/theories/Program/Basics.v b/theories/Program/Basics.v index 0a4b15d29d..69e3206ba4 100644 --- a/theories/Program/Basics.v +++ b/theories/Program/Basics.v @@ -6,8 +6,6 @@ (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) - (** Standard functions and combinators. Proofs about them require functional extensionality and can be found diff --git a/theories/Program/Combinators.v b/theories/Program/Combinators.v index 31661b9d37..8d041422d8 100644 --- a/theories/Program/Combinators.v +++ b/theories/Program/Combinators.v @@ -6,8 +6,6 @@ (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) - (** * Proofs about standard combinators, exports functional extensionality. Author: Matthieu Sozeau diff --git a/theories/Program/Equality.v b/theories/Program/Equality.v index c3c5f9c95e..5a047ec5ce 100644 --- a/theories/Program/Equality.v +++ b/theories/Program/Equality.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - (** Tactics related to (dependent) equality and proof irrelevance. *) Require Export ProofIrrelevance. diff --git a/theories/Program/Program.v b/theories/Program/Program.v index cdfc785837..ffdd1bd55b 100644 --- a/theories/Program/Program.v +++ b/theories/Program/Program.v @@ -5,8 +5,6 @@ (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) - Require Export Coq.Program.Utils. Require Export Coq.Program.Wf. Require Export Coq.Program.Equality. diff --git a/theories/Program/Subset.v b/theories/Program/Subset.v index 89f477d8f9..523171013b 100644 --- a/theories/Program/Subset.v +++ b/theories/Program/Subset.v @@ -5,8 +5,6 @@ (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) - (** Tactics related to subsets and proof irrelevance. *) Require Import Coq.Program.Utils. diff --git a/theories/Program/Syntax.v b/theories/Program/Syntax.v index 916c33ee62..2c5fb79c56 100644 --- a/theories/Program/Syntax.v +++ b/theories/Program/Syntax.v @@ -5,8 +5,6 @@ (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) - (** Custom notations and implicits for Coq prelude definitions. Author: Matthieu Sozeau diff --git a/theories/Program/Tactics.v b/theories/Program/Tactics.v index d187941d20..f4d53c2791 100644 --- a/theories/Program/Tactics.v +++ b/theories/Program/Tactics.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - (** This module implements various tactics used to simplify the goals produced by Program, which are also generally useful. *) diff --git a/theories/Program/Utils.v b/theories/Program/Utils.v index fbf0b03cf8..dbcaea80fd 100644 --- a/theories/Program/Utils.v +++ b/theories/Program/Utils.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - (** Various syntaxic shortands that are useful with [Program]. *) Require Export Coq.Program.Tactics. diff --git a/theories/Program/Wf.v b/theories/Program/Wf.v index c4d06fd722..70a6fe97a4 100644 --- a/theories/Program/Wf.v +++ b/theories/Program/Wf.v @@ -5,8 +5,6 @@ (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) - (** Reformulation of the Wf module using subsets where possible, providing the support for [Program]'s treatment of well-founded definitions. *) diff --git a/theories/QArith/QArith.v b/theories/QArith/QArith.v index f7a28598ee..fe1ff3674e 100644 --- a/theories/QArith/QArith.v +++ b/theories/QArith/QArith.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - Require Export QArith_base. Require Export Qring. Require Export Qreduction. diff --git a/theories/QArith/QArith_base.v b/theories/QArith/QArith_base.v index 609241d5e8..111d2391aa 100644 --- a/theories/QArith/QArith_base.v +++ b/theories/QArith/QArith_base.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - Require Export ZArith. Require Export ZArithRing. Require Export Morphisms Setoid Bool. diff --git a/theories/QArith/Qcanon.v b/theories/QArith/Qcanon.v index 34d6267e34..b26b828ca9 100644 --- a/theories/QArith/Qcanon.v +++ b/theories/QArith/Qcanon.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - Require Import Field. Require Import QArith. Require Import Znumtheory. diff --git a/theories/QArith/Qfield.v b/theories/QArith/Qfield.v index fbfae55c3f..524996c38e 100644 --- a/theories/QArith/Qfield.v +++ b/theories/QArith/Qfield.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - Require Export Field. Require Export QArith_base. Require Import NArithRing. diff --git a/theories/QArith/Qreals.v b/theories/QArith/Qreals.v index 12e371ee9e..15fea85168 100644 --- a/theories/QArith/Qreals.v +++ b/theories/QArith/Qreals.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - Require Export Rbase. Require Export QArith_base. diff --git a/theories/QArith/Qreduction.v b/theories/QArith/Qreduction.v index 27e3c4e02a..4f16f5b8c2 100644 --- a/theories/QArith/Qreduction.v +++ b/theories/QArith/Qreduction.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - (** Normalisation functions for rational numbers. *) Require Export QArith_base. diff --git a/theories/QArith/Qring.v b/theories/QArith/Qring.v index 8c9e2dfa3b..96ed046a65 100644 --- a/theories/QArith/Qring.v +++ b/theories/QArith/Qring.v @@ -6,6 +6,4 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - Require Export Qfield. diff --git a/theories/Reals/Alembert.v b/theories/Reals/Alembert.v index ef75323e08..1b9be07956 100644 --- a/theories/Reals/Alembert.v +++ b/theories/Reals/Alembert.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - Require Import Rbase. Require Import Rfunctions. Require Import Rseries. diff --git a/theories/Reals/AltSeries.v b/theories/Reals/AltSeries.v index cccc8ceec1..9c29e26a3b 100644 --- a/theories/Reals/AltSeries.v +++ b/theories/Reals/AltSeries.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) - (*i $Id$ i*) - Require Import Rbase. Require Import Rfunctions. Require Import Rseries. diff --git a/theories/Reals/ArithProp.v b/theories/Reals/ArithProp.v index f22ff5cb25..48324e8e8e 100644 --- a/theories/Reals/ArithProp.v +++ b/theories/Reals/ArithProp.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) - (*i $Id$ i*) - Require Import Rbase. Require Import Rbasic_fun. Require Import Even. diff --git a/theories/Reals/Binomial.v b/theories/Reals/Binomial.v index 0d34d22c55..d0df984a12 100644 --- a/theories/Reals/Binomial.v +++ b/theories/Reals/Binomial.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) - (*i $Id$ i*) - Require Import Rbase. Require Import Rfunctions. Require Import PartSum. diff --git a/theories/Reals/Cauchy_prod.v b/theories/Reals/Cauchy_prod.v index 6ea0767d09..68a842c9fc 100644 --- a/theories/Reals/Cauchy_prod.v +++ b/theories/Reals/Cauchy_prod.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) - (*i $Id$ i*) - Require Import Rbase. Require Import Rfunctions. Require Import Rseries. diff --git a/theories/Reals/Cos_plus.v b/theories/Reals/Cos_plus.v index 6c08356a75..c5e2c0ed31 100644 --- a/theories/Reals/Cos_plus.v +++ b/theories/Reals/Cos_plus.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) - (*i $Id$ i*) - Require Import Rbase. Require Import Rfunctions. Require Import SeqSeries. diff --git a/theories/Reals/Cos_rel.v b/theories/Reals/Cos_rel.v index 7a893c53c3..d27e0ae4c6 100644 --- a/theories/Reals/Cos_rel.v +++ b/theories/Reals/Cos_rel.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - Require Import Rbase. Require Import Rfunctions. Require Import SeqSeries. diff --git a/theories/Reals/DiscrR.v b/theories/Reals/DiscrR.v index e037c77b59..0d41b59000 100644 --- a/theories/Reals/DiscrR.v +++ b/theories/Reals/DiscrR.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - Require Import RIneq. Require Import Omega. Open Local Scope R_scope. diff --git a/theories/Reals/Exp_prop.v b/theories/Reals/Exp_prop.v index 1c74f55a0d..287057f0fd 100644 --- a/theories/Reals/Exp_prop.v +++ b/theories/Reals/Exp_prop.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - Require Import Rbase. Require Import Rfunctions. Require Import SeqSeries. diff --git a/theories/Reals/Integration.v b/theories/Reals/Integration.v index 774a0bd5cd..eba81ff9b6 100644 --- a/theories/Reals/Integration.v +++ b/theories/Reals/Integration.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - Require Export NewtonInt. Require Export RiemannInt_SF. Require Export RiemannInt.
\ No newline at end of file diff --git a/theories/Reals/LegacyRfield.v b/theories/Reals/LegacyRfield.v index b33274af92..ca7cb8feab 100644 --- a/theories/Reals/LegacyRfield.v +++ b/theories/Reals/LegacyRfield.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - Require Export Raxioms. Require Export LegacyField. Import LegacyRing_theory. diff --git a/theories/Reals/MVT.v b/theories/Reals/MVT.v index 4037e3dece..72bd62a699 100644 --- a/theories/Reals/MVT.v +++ b/theories/Reals/MVT.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - Require Import Rbase. Require Import Rfunctions. Require Import Ranalysis1. diff --git a/theories/Reals/NewtonInt.v b/theories/Reals/NewtonInt.v index 74bcf7dcd1..0d75a9dee4 100644 --- a/theories/Reals/NewtonInt.v +++ b/theories/Reals/NewtonInt.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - Require Import Rbase. Require Import Rfunctions. Require Import SeqSeries. diff --git a/theories/Reals/PSeries_reg.v b/theories/Reals/PSeries_reg.v index 97793386de..80a5b87a83 100644 --- a/theories/Reals/PSeries_reg.v +++ b/theories/Reals/PSeries_reg.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - Require Import Rbase. Require Import Rfunctions. Require Import SeqSeries. diff --git a/theories/Reals/PartSum.v b/theories/Reals/PartSum.v index 6a33b80928..e9a224b978 100644 --- a/theories/Reals/PartSum.v +++ b/theories/Reals/PartSum.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - Require Import Rbase. Require Import Rfunctions. Require Import Rseries. diff --git a/theories/Reals/RIneq.v b/theories/Reals/RIneq.v index 2b6af10ecf..7c45556054 100644 --- a/theories/Reals/RIneq.v +++ b/theories/Reals/RIneq.v @@ -7,8 +7,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - (*********************************************************) (** * Basic lemmas for the classical real numbers *) (*********************************************************) diff --git a/theories/Reals/RList.v b/theories/Reals/RList.v index 545bd68b2c..8cf56cd7bf 100644 --- a/theories/Reals/RList.v +++ b/theories/Reals/RList.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - Require Import Rbase. Require Import Rfunctions. Open Local Scope R_scope. diff --git a/theories/Reals/R_Ifp.v b/theories/Reals/R_Ifp.v index 57b2c76756..e530070b1a 100644 --- a/theories/Reals/R_Ifp.v +++ b/theories/Reals/R_Ifp.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - (**********************************************************) (** Complements for the reals.Integer and fractional part *) (* *) diff --git a/theories/Reals/R_sqr.v b/theories/Reals/R_sqr.v index 6460a92719..1cccb88487 100644 --- a/theories/Reals/R_sqr.v +++ b/theories/Reals/R_sqr.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - Require Import Rbase. Require Import Rbasic_fun. Open Local Scope R_scope. diff --git a/theories/Reals/R_sqrt.v b/theories/Reals/R_sqrt.v index 2c43ee9b9e..13232566f1 100644 --- a/theories/Reals/R_sqrt.v +++ b/theories/Reals/R_sqrt.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - Require Import Rbase. Require Import Rfunctions. Require Import Rsqrt_def. diff --git a/theories/Reals/Ranalysis.v b/theories/Reals/Ranalysis.v index 500dd5295d..53267174b1 100644 --- a/theories/Reals/Ranalysis.v +++ b/theories/Reals/Ranalysis.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - Require Import Rbase. Require Import Rfunctions. Require Import Rtrigo. diff --git a/theories/Reals/Ranalysis1.v b/theories/Reals/Ranalysis1.v index 1516b3384e..a0b10c8911 100644 --- a/theories/Reals/Ranalysis1.v +++ b/theories/Reals/Ranalysis1.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - Require Import Rbase. Require Import Rfunctions. Require Export Rlimit. diff --git a/theories/Reals/Ranalysis2.v b/theories/Reals/Ranalysis2.v index 1d44b3e731..04c00cb301 100644 --- a/theories/Reals/Ranalysis2.v +++ b/theories/Reals/Ranalysis2.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - Require Import Rbase. Require Import Rfunctions. Require Import Ranalysis1. diff --git a/theories/Reals/Ranalysis3.v b/theories/Reals/Ranalysis3.v index 3b685cd8a0..28da1c7c4c 100644 --- a/theories/Reals/Ranalysis3.v +++ b/theories/Reals/Ranalysis3.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - Require Import Rbase. Require Import Rfunctions. Require Import Ranalysis1. diff --git a/theories/Reals/Ranalysis4.v b/theories/Reals/Ranalysis4.v index 1ed3fb7135..abf0b883fd 100644 --- a/theories/Reals/Ranalysis4.v +++ b/theories/Reals/Ranalysis4.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - Require Import Rbase. Require Import Rfunctions. Require Import SeqSeries. diff --git a/theories/Reals/Raxioms.v b/theories/Reals/Raxioms.v index 9715414f5e..1ed75cdb68 100644 --- a/theories/Reals/Raxioms.v +++ b/theories/Reals/Raxioms.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - (*********************************************************) (** Axiomatisation of the classical reals *) (*********************************************************) diff --git a/theories/Reals/Rbase.v b/theories/Reals/Rbase.v index ab1c074748..8843c5e6ea 100644 --- a/theories/Reals/Rbase.v +++ b/theories/Reals/Rbase.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - Require Export Rdefinitions. Require Export Raxioms. Require Export RIneq. diff --git a/theories/Reals/Rbasic_fun.v b/theories/Reals/Rbasic_fun.v index 7588020c53..2e1bd0797b 100644 --- a/theories/Reals/Rbasic_fun.v +++ b/theories/Reals/Rbasic_fun.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - (*********************************************************) (** Complements for the real numbers *) (* *) diff --git a/theories/Reals/Rcomplete.v b/theories/Reals/Rcomplete.v index 27d5c49efb..de32505291 100644 --- a/theories/Reals/Rcomplete.v +++ b/theories/Reals/Rcomplete.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - Require Import Rbase. Require Import Rfunctions. Require Import Rseries. diff --git a/theories/Reals/Rdefinitions.v b/theories/Reals/Rdefinitions.v index 023cfc93c3..ab6ed8b10a 100644 --- a/theories/Reals/Rdefinitions.v +++ b/theories/Reals/Rdefinitions.v @@ -5,8 +5,6 @@ (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - (*********************************************************) (** Definitions for the axiomatization *) diff --git a/theories/Reals/Rderiv.v b/theories/Reals/Rderiv.v index 6413943a90..19ebcd3cb1 100644 --- a/theories/Reals/Rderiv.v +++ b/theories/Reals/Rderiv.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - (*********************************************************) (** Definition of the derivative,continuity *) (* *) diff --git a/theories/Reals/Reals.v b/theories/Reals/Reals.v index d18213db49..de57a5af2a 100644 --- a/theories/Reals/Reals.v +++ b/theories/Reals/Reals.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - (** The library REALS is divided in 6 parts : - Rbase: basic lemmas on R equalities and inequalities diff --git a/theories/Reals/Rfunctions.v b/theories/Reals/Rfunctions.v index 7371c8acf3..6688913694 100644 --- a/theories/Reals/Rfunctions.v +++ b/theories/Reals/Rfunctions.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - (*i Some properties about pow and sum have been made with John Harrison i*) (*i Some Lemmas (about pow and powerRZ) have been done by Laurent Thery i*) diff --git a/theories/Reals/Rgeom.v b/theories/Reals/Rgeom.v index 8890cbb508..dceb98d45f 100644 --- a/theories/Reals/Rgeom.v +++ b/theories/Reals/Rgeom.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - Require Import Rbase. Require Import Rfunctions. Require Import SeqSeries. diff --git a/theories/Reals/RiemannInt.v b/theories/Reals/RiemannInt.v index 9fd6e00882..abf817d7a1 100644 --- a/theories/Reals/RiemannInt.v +++ b/theories/Reals/RiemannInt.v @@ -7,8 +7,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - Require Import Rfunctions. Require Import SeqSeries. Require Import Ranalysis. diff --git a/theories/Reals/RiemannInt_SF.v b/theories/Reals/RiemannInt_SF.v index f9b1b890f7..f783d1d827 100644 --- a/theories/Reals/RiemannInt_SF.v +++ b/theories/Reals/RiemannInt_SF.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - Require Import Rbase. Require Import Rfunctions. Require Import Ranalysis. diff --git a/theories/Reals/Rlimit.v b/theories/Reals/Rlimit.v index 3aaa7300a9..e0f47364fd 100644 --- a/theories/Reals/Rlimit.v +++ b/theories/Reals/Rlimit.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - (*********************************************************) (** Definition of the limit *) (* *) diff --git a/theories/Reals/Rpow_def.v b/theories/Reals/Rpow_def.v index c7d1893be0..f922e25f62 100644 --- a/theories/Reals/Rpow_def.v +++ b/theories/Reals/Rpow_def.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) - Require Import Rdefinitions. Fixpoint pow (r:R) (n:nat) : R := diff --git a/theories/Reals/Rpower.v b/theories/Reals/Rpower.v index a4feed8f3e..957466cbe4 100644 --- a/theories/Reals/Rpower.v +++ b/theories/Reals/Rpower.v @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) (*i Due to L.Thery i*) (************************************************************) diff --git a/theories/Reals/Rprod.v b/theories/Reals/Rprod.v index bb3df6bb8e..4e3f4d0896 100644 --- a/theories/Reals/Rprod.v +++ b/theories/Reals/Rprod.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - Require Import Compare. Require Import Rbase. Require Import Rfunctions. diff --git a/theories/Reals/Rseries.v b/theories/Reals/Rseries.v index 1ed6b03c53..9e51220622 100644 --- a/theories/Reals/Rseries.v +++ b/theories/Reals/Rseries.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - Require Import Rbase. Require Import Rfunctions. Require Import Compare. diff --git a/theories/Reals/Rsigma.v b/theories/Reals/Rsigma.v index 9175927029..155577746a 100644 --- a/theories/Reals/Rsigma.v +++ b/theories/Reals/Rsigma.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - Require Import Rbase. Require Import Rfunctions. Require Import Rseries. diff --git a/theories/Reals/Rsqrt_def.v b/theories/Reals/Rsqrt_def.v index 33c20355cc..a8f12a6b39 100644 --- a/theories/Reals/Rsqrt_def.v +++ b/theories/Reals/Rsqrt_def.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - Require Import Sumbool. Require Import Rbase. Require Import Rfunctions. diff --git a/theories/Reals/Rtopology.v b/theories/Reals/Rtopology.v index 5b55896b17..a086cfd46c 100644 --- a/theories/Reals/Rtopology.v +++ b/theories/Reals/Rtopology.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - Require Import Rbase. Require Import Rfunctions. Require Import Ranalysis1. diff --git a/theories/Reals/Rtrigo.v b/theories/Reals/Rtrigo.v index 4981d6fdf1..582b6be759 100644 --- a/theories/Reals/Rtrigo.v +++ b/theories/Reals/Rtrigo.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - Require Import Rbase. Require Import Rfunctions. Require Import SeqSeries. diff --git a/theories/Reals/Rtrigo_alt.v b/theories/Reals/Rtrigo_alt.v index fe2da83911..1cf0944c08 100644 --- a/theories/Reals/Rtrigo_alt.v +++ b/theories/Reals/Rtrigo_alt.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - Require Import Rbase. Require Import Rfunctions. Require Import SeqSeries. diff --git a/theories/Reals/Rtrigo_calc.v b/theories/Reals/Rtrigo_calc.v index a7fddb4731..33ea1adba0 100644 --- a/theories/Reals/Rtrigo_calc.v +++ b/theories/Reals/Rtrigo_calc.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - Require Import Rbase. Require Import Rfunctions. Require Import SeqSeries. diff --git a/theories/Reals/Rtrigo_def.v b/theories/Reals/Rtrigo_def.v index 9588e44380..265dae9d4f 100644 --- a/theories/Reals/Rtrigo_def.v +++ b/theories/Reals/Rtrigo_def.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - Require Import Rbase. Require Import Rfunctions. Require Import SeqSeries. diff --git a/theories/Reals/Rtrigo_fun.v b/theories/Reals/Rtrigo_fun.v index cb53b5346e..62d8d9f5fd 100644 --- a/theories/Reals/Rtrigo_fun.v +++ b/theories/Reals/Rtrigo_fun.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - Require Import Rbase. Require Import Rfunctions. Require Import SeqSeries. diff --git a/theories/Reals/Rtrigo_reg.v b/theories/Reals/Rtrigo_reg.v index 5b731488b1..f38e59e824 100644 --- a/theories/Reals/Rtrigo_reg.v +++ b/theories/Reals/Rtrigo_reg.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - Require Import Rbase. Require Import Rfunctions. Require Import SeqSeries. diff --git a/theories/Reals/SeqProp.v b/theories/Reals/SeqProp.v index 82647c8378..642e7fc9e2 100644 --- a/theories/Reals/SeqProp.v +++ b/theories/Reals/SeqProp.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - Require Import Rbase. Require Import Rfunctions. Require Import Rseries. diff --git a/theories/Reals/SeqSeries.v b/theories/Reals/SeqSeries.v index dbfc85bb94..dcfadd566d 100644 --- a/theories/Reals/SeqSeries.v +++ b/theories/Reals/SeqSeries.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - Require Import Rbase. Require Import Rfunctions. Require Import Max. diff --git a/theories/Reals/SplitAbsolu.v b/theories/Reals/SplitAbsolu.v index 5882f953c4..90048e50d9 100644 --- a/theories/Reals/SplitAbsolu.v +++ b/theories/Reals/SplitAbsolu.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - Require Import Rbasic_fun. Ltac split_case_Rabs := diff --git a/theories/Reals/SplitRmult.v b/theories/Reals/SplitRmult.v index 51e54860d2..322808f9b5 100644 --- a/theories/Reals/SplitRmult.v +++ b/theories/Reals/SplitRmult.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - (*i Lemma mult_non_zero :(r1,r2:R)``r1<>0`` /\ ``r2<>0`` -> ``r1*r2<>0``. i*) diff --git a/theories/Reals/Sqrt_reg.v b/theories/Reals/Sqrt_reg.v index 4f336648b9..3961b8b0ce 100644 --- a/theories/Reals/Sqrt_reg.v +++ b/theories/Reals/Sqrt_reg.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - Require Import Rbase. Require Import Rfunctions. Require Import Ranalysis1. diff --git a/theories/Relations/Operators_Properties.v b/theories/Relations/Operators_Properties.v index 1976b435c1..cfb9526324 100644 --- a/theories/Relations/Operators_Properties.v +++ b/theories/Relations/Operators_Properties.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - (************************************************************************) (** * Some properties of the operators on relations *) (************************************************************************) diff --git a/theories/Relations/Relation_Definitions.v b/theories/Relations/Relation_Definitions.v index c03c4b95f9..4f676484ab 100644 --- a/theories/Relations/Relation_Definitions.v +++ b/theories/Relations/Relation_Definitions.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - Section Relation_Definition. Variable A : Type. diff --git a/theories/Relations/Relation_Operators.v b/theories/Relations/Relation_Operators.v index 39e0331d59..bdc44dd176 100644 --- a/theories/Relations/Relation_Operators.v +++ b/theories/Relations/Relation_Operators.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - (************************************************************************) (** * Bruno Barras, Cristina Cornes *) (** * *) diff --git a/theories/Relations/Relations.v b/theories/Relations/Relations.v index 1c6df08a46..f1e20b10e7 100644 --- a/theories/Relations/Relations.v +++ b/theories/Relations/Relations.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - Require Export Relation_Definitions. Require Export Relation_Operators. Require Export Operators_Properties. diff --git a/theories/Setoids/Setoid.v b/theories/Setoids/Setoid.v index c5530e7ca4..cf641253aa 100644 --- a/theories/Setoids/Setoid.v +++ b/theories/Setoids/Setoid.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$: i*) - Require Export Coq.Classes.SetoidTactics. Export Morphisms.ProperNotations. diff --git a/theories/Sets/Classical_sets.v b/theories/Sets/Classical_sets.v index 5f68609970..5fbfadd4c2 100644 --- a/theories/Sets/Classical_sets.v +++ b/theories/Sets/Classical_sets.v @@ -24,8 +24,6 @@ (* in Summer 1995. Several developments by E. Ledinot were an inspiration. *) (****************************************************************************) -(*i $Id$ i*) - Require Export Ensembles. Require Export Constructive_sets. Require Export Classical_Type. diff --git a/theories/Sets/Constructive_sets.v b/theories/Sets/Constructive_sets.v index 0719365f14..294dbb0cd2 100644 --- a/theories/Sets/Constructive_sets.v +++ b/theories/Sets/Constructive_sets.v @@ -24,8 +24,6 @@ (* in Summer 1995. Several developments by E. Ledinot were an inspiration. *) (****************************************************************************) -(*i $Id$ i*) - Require Export Ensembles. Section Ensembles_facts. diff --git a/theories/Sets/Cpo.v b/theories/Sets/Cpo.v index 8c69e68771..6d537f59bb 100644 --- a/theories/Sets/Cpo.v +++ b/theories/Sets/Cpo.v @@ -24,8 +24,6 @@ (* in Summer 1995. Several developments by E. Ledinot were an inspiration. *) (****************************************************************************) -(*i $Id$ i*) - Require Export Ensembles. Require Export Relations_1. Require Export Partial_Order. diff --git a/theories/Sets/Ensembles.v b/theories/Sets/Ensembles.v index 0fa9c74a82..8843cadd62 100644 --- a/theories/Sets/Ensembles.v +++ b/theories/Sets/Ensembles.v @@ -24,8 +24,6 @@ (* in Summer 1995. Several developments by E. Ledinot were an inspiration. *) (****************************************************************************) -(*i $Id$ i*) - Section Ensembles. Variable U : Type. diff --git a/theories/Sets/Finite_sets.v b/theories/Sets/Finite_sets.v index 019c25a556..11ac3b9e49 100644 --- a/theories/Sets/Finite_sets.v +++ b/theories/Sets/Finite_sets.v @@ -24,8 +24,6 @@ (* in Summer 1995. Several developments by E. Ledinot were an inspiration. *) (****************************************************************************) -(*i $Id$ i*) - Require Import Ensembles. Section Ensembles_finis. diff --git a/theories/Sets/Finite_sets_facts.v b/theories/Sets/Finite_sets_facts.v index fdcc4150ff..da4a358130 100644 --- a/theories/Sets/Finite_sets_facts.v +++ b/theories/Sets/Finite_sets_facts.v @@ -24,8 +24,6 @@ (* in Summer 1995. Several developments by E. Ledinot were an inspiration. *) (****************************************************************************) -(*i $Id$ i*) - Require Export Finite_sets. Require Export Constructive_sets. Require Export Classical_Type. diff --git a/theories/Sets/Image.v b/theories/Sets/Image.v index 64c341bd37..313a18dcc0 100644 --- a/theories/Sets/Image.v +++ b/theories/Sets/Image.v @@ -24,8 +24,6 @@ (* in Summer 1995. Several developments by E. Ledinot were an inspiration. *) (****************************************************************************) -(*i $Id$ i*) - Require Export Finite_sets. Require Export Constructive_sets. Require Export Classical_Type. diff --git a/theories/Sets/Infinite_sets.v b/theories/Sets/Infinite_sets.v index b63ec1d472..0ae11b4f6d 100644 --- a/theories/Sets/Infinite_sets.v +++ b/theories/Sets/Infinite_sets.v @@ -24,8 +24,6 @@ (* in Summer 1995. Several developments by E. Ledinot were an inspiration. *) (****************************************************************************) -(*i $Id$ i*) - Require Export Finite_sets. Require Export Constructive_sets. Require Export Classical_Type. diff --git a/theories/Sets/Integers.v b/theories/Sets/Integers.v index 15c1b665eb..8fe9928b18 100644 --- a/theories/Sets/Integers.v +++ b/theories/Sets/Integers.v @@ -24,8 +24,6 @@ (* in Summer 1995. Several developments by E. Ledinot were an inspiration. *) (****************************************************************************) -(*i $Id$ i*) - Require Export Finite_sets. Require Export Constructive_sets. Require Export Classical_Type. diff --git a/theories/Sets/Multiset.v b/theories/Sets/Multiset.v index 7216ae335c..5b7aa24b7b 100644 --- a/theories/Sets/Multiset.v +++ b/theories/Sets/Multiset.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - (* G. Huet 1-9-95 *) Require Import Permut Setoid. diff --git a/theories/Sets/Partial_Order.v b/theories/Sets/Partial_Order.v index 4fe8f4f6a4..195f454e5f 100644 --- a/theories/Sets/Partial_Order.v +++ b/theories/Sets/Partial_Order.v @@ -24,8 +24,6 @@ (* in Summer 1995. Several developments by E. Ledinot were an inspiration. *) (****************************************************************************) -(*i $Id$ i*) - Require Export Ensembles. Require Export Relations_1. diff --git a/theories/Sets/Permut.v b/theories/Sets/Permut.v index f593031a0f..25a121cb3b 100644 --- a/theories/Sets/Permut.v +++ b/theories/Sets/Permut.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - (* G. Huet 1-9-95 *) (** We consider a Set [U], given with a commutative-associative operator [op], diff --git a/theories/Sets/Powerset.v b/theories/Sets/Powerset.v index c323ca3569..9ecb600a5d 100644 --- a/theories/Sets/Powerset.v +++ b/theories/Sets/Powerset.v @@ -24,8 +24,6 @@ (* in Summer 1995. Several developments by E. Ledinot were an inspiration. *) (****************************************************************************) -(*i $Id$ i*) - Require Export Ensembles. Require Export Relations_1. Require Export Relations_1_facts. diff --git a/theories/Sets/Powerset_Classical_facts.v b/theories/Sets/Powerset_Classical_facts.v index 36d2150c3d..8f881c3634 100644 --- a/theories/Sets/Powerset_Classical_facts.v +++ b/theories/Sets/Powerset_Classical_facts.v @@ -24,8 +24,6 @@ (* in Summer 1995. Several developments by E. Ledinot were an inspiration. *) (****************************************************************************) -(*i $Id$ i*) - Require Export Ensembles. Require Export Constructive_sets. Require Export Relations_1. diff --git a/theories/Sets/Powerset_facts.v b/theories/Sets/Powerset_facts.v index 76f7f1ec89..61f783957c 100644 --- a/theories/Sets/Powerset_facts.v +++ b/theories/Sets/Powerset_facts.v @@ -24,8 +24,6 @@ (* in Summer 1995. Several developments by E. Ledinot were an inspiration. *) (****************************************************************************) -(*i $Id$ i*) - Require Export Ensembles. Require Export Constructive_sets. Require Export Relations_1. diff --git a/theories/Sets/Relations_1.v b/theories/Sets/Relations_1.v index 85d0cffccc..eb3273959d 100644 --- a/theories/Sets/Relations_1.v +++ b/theories/Sets/Relations_1.v @@ -24,8 +24,6 @@ (* in Summer 1995. Several developments by E. Ledinot were an inspiration. *) (****************************************************************************) -(*i $Id$ i*) - Section Relations_1. Variable U : Type. diff --git a/theories/Sets/Relations_1_facts.v b/theories/Sets/Relations_1_facts.v index fd83b0e0df..484245bc84 100644 --- a/theories/Sets/Relations_1_facts.v +++ b/theories/Sets/Relations_1_facts.v @@ -24,8 +24,6 @@ (* in Summer 1995. Several developments by E. Ledinot were an inspiration. *) (****************************************************************************) -(*i $Id$ i*) - Require Export Relations_1. Definition Complement (U:Type) (R:Relation U) : Relation U := diff --git a/theories/Sets/Relations_2.v b/theories/Sets/Relations_2.v index 11ac85e845..3b1e7057dd 100644 --- a/theories/Sets/Relations_2.v +++ b/theories/Sets/Relations_2.v @@ -24,8 +24,6 @@ (* in Summer 1995. Several developments by E. Ledinot were an inspiration. *) (****************************************************************************) -(*i $Id$ i*) - Require Export Relations_1. Section Relations_2. diff --git a/theories/Sets/Relations_2_facts.v b/theories/Sets/Relations_2_facts.v index 3554901b93..6fd07160f0 100644 --- a/theories/Sets/Relations_2_facts.v +++ b/theories/Sets/Relations_2_facts.v @@ -24,8 +24,6 @@ (* in Summer 1995. Several developments by E. Ledinot were an inspiration. *) (****************************************************************************) -(*i $Id$ i*) - Require Export Relations_1. Require Export Relations_1_facts. Require Export Relations_2. diff --git a/theories/Sets/Relations_3.v b/theories/Sets/Relations_3.v index 970db1827b..991b382425 100644 --- a/theories/Sets/Relations_3.v +++ b/theories/Sets/Relations_3.v @@ -24,8 +24,6 @@ (* in Summer 1995. Several developments by E. Ledinot were an inspiration. *) (****************************************************************************) -(*i $Id$ i*) - Require Export Relations_1. Require Export Relations_2. diff --git a/theories/Sets/Relations_3_facts.v b/theories/Sets/Relations_3_facts.v index d8bf7dc3c7..a2a0f4584c 100644 --- a/theories/Sets/Relations_3_facts.v +++ b/theories/Sets/Relations_3_facts.v @@ -24,8 +24,6 @@ (* in Summer 1995. Several developments by E. Ledinot were an inspiration. *) (****************************************************************************) -(*i $Id$ i*) - Require Export Relations_1. Require Export Relations_1_facts. Require Export Relations_2. diff --git a/theories/Sets/Uniset.v b/theories/Sets/Uniset.v index 909c798380..41e7f0edf9 100644 --- a/theories/Sets/Uniset.v +++ b/theories/Sets/Uniset.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - (** Sets as characteristic functions *) (* G. Huet 1-9-95 *) diff --git a/theories/Sorting/Heap.v b/theories/Sorting/Heap.v index 4124ef9832..c48d22d62e 100644 --- a/theories/Sorting/Heap.v +++ b/theories/Sorting/Heap.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - (** This file is deprecated, for a tree on list, use [Mergesort.v]. *) (** A development of Treesort on Heap trees. It has an average diff --git a/theories/Sorting/Mergesort.v b/theories/Sorting/Mergesort.v index 238013b854..5830fabe46 100644 --- a/theories/Sorting/Mergesort.v +++ b/theories/Sorting/Mergesort.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - (** A modular implementation of mergesort (the complexity is O(n.log n) in the length of the list) *) diff --git a/theories/Sorting/PermutEq.v b/theories/Sorting/PermutEq.v index 8e6aa6dce6..6ad0b6ba09 100644 --- a/theories/Sorting/PermutEq.v +++ b/theories/Sorting/PermutEq.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - Require Import Relations Setoid SetoidList List Multiset PermutSetoid Permutation. Set Implicit Arguments. diff --git a/theories/Sorting/PermutSetoid.v b/theories/Sorting/PermutSetoid.v index 203e212b68..5faaebe285 100644 --- a/theories/Sorting/PermutSetoid.v +++ b/theories/Sorting/PermutSetoid.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - Require Import Omega Relations Multiset SetoidList. (** This file is deprecated, use [Permutation.v] instead. diff --git a/theories/Sorting/Permutation.v b/theories/Sorting/Permutation.v index c3cd4f4a8f..e861b9ce7a 100644 --- a/theories/Sorting/Permutation.v +++ b/theories/Sorting/Permutation.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - (*********************************************************************) (** ** List permutations as a composition of adjacent transpositions *) (*********************************************************************) diff --git a/theories/Sorting/Sorted.v b/theories/Sorting/Sorted.v index d87259eec6..931e29bf8d 100644 --- a/theories/Sorting/Sorted.v +++ b/theories/Sorting/Sorted.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - (* Made by Hugo Herbelin *) (** This file defines two notions of sorted list: diff --git a/theories/Sorting/Sorting.v b/theories/Sorting/Sorting.v index 5f8da6a4dc..f05cc473b7 100644 --- a/theories/Sorting/Sorting.v +++ b/theories/Sorting/Sorting.v @@ -6,7 +6,5 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - Require Export Sorted. Require Export Mergesort. diff --git a/theories/Strings/Ascii.v b/theories/Strings/Ascii.v index 1f90c06cfc..ba01f3d4c3 100644 --- a/theories/Strings/Ascii.v +++ b/theories/Strings/Ascii.v @@ -7,8 +7,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) - (** Contributed by Laurent Théry (INRIA); Adapted to Coq V8 by the Coq Development Team *) diff --git a/theories/Strings/String.v b/theories/Strings/String.v index 15f2982184..c6bf9e1198 100644 --- a/theories/Strings/String.v +++ b/theories/Strings/String.v @@ -7,8 +7,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) - (** Contributed by Laurent Théry (INRIA); Adapted to Coq V8 by the Coq Development Team *) diff --git a/theories/Structures/DecidableType.v b/theories/Structures/DecidableType.v index 2c72e30b16..79e817717a 100644 --- a/theories/Structures/DecidableType.v +++ b/theories/Structures/DecidableType.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) -(* $Id$ *) - Require Export SetoidList. Require Equalities. diff --git a/theories/Structures/DecidableTypeEx.v b/theories/Structures/DecidableTypeEx.v index 4407ead416..2c02f8ddd1 100644 --- a/theories/Structures/DecidableTypeEx.v +++ b/theories/Structures/DecidableTypeEx.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) -(* $Id$ *) - Require Import DecidableType OrderedType OrderedTypeEx. Set Implicit Arguments. Unset Strict Implicit. diff --git a/theories/Structures/Equalities.v b/theories/Structures/Equalities.v index 3d4430b9e8..0a6dba982a 100644 --- a/theories/Structures/Equalities.v +++ b/theories/Structures/Equalities.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) -(* $Id$ *) - Require Export RelationClasses. Set Implicit Arguments. diff --git a/theories/Structures/OrderedType.v b/theories/Structures/OrderedType.v index 72fbe79680..6b9007fdd3 100644 --- a/theories/Structures/OrderedType.v +++ b/theories/Structures/OrderedType.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) -(* $Id$ *) - Require Export SetoidList Morphisms OrdersTac. Set Implicit Arguments. Unset Strict Implicit. diff --git a/theories/Structures/OrderedTypeAlt.v b/theories/Structures/OrderedTypeAlt.v index 23ae4c85a3..b054496e9a 100644 --- a/theories/Structures/OrderedTypeAlt.v +++ b/theories/Structures/OrderedTypeAlt.v @@ -5,8 +5,6 @@ (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) -(* $Id$ *) - Require Import OrderedType. (** * An alternative (but equivalent) presentation for an Ordered Type diff --git a/theories/Structures/OrderedTypeEx.v b/theories/Structures/OrderedTypeEx.v index a39f336a57..600eabf110 100644 --- a/theories/Structures/OrderedTypeEx.v +++ b/theories/Structures/OrderedTypeEx.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) -(* $Id$ *) - Require Import OrderedType. Require Import ZArith. Require Import Omega. diff --git a/theories/Structures/Orders.v b/theories/Structures/Orders.v index 96daca5cd3..d7bdfbf717 100644 --- a/theories/Structures/Orders.v +++ b/theories/Structures/Orders.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) -(* $Id$ *) - Require Export Relations Morphisms Setoid Equalities. Set Implicit Arguments. Unset Strict Implicit. diff --git a/theories/Structures/OrdersAlt.v b/theories/Structures/OrdersAlt.v index d86b02a15e..85e7fb176e 100644 --- a/theories/Structures/OrdersAlt.v +++ b/theories/Structures/OrdersAlt.v @@ -11,8 +11,6 @@ * Institution: LRI, CNRS UMR 8623 - Université Paris Sud * 91405 Orsay, France *) -(* $Id$ *) - Require Import OrderedType Orders. Set Implicit Arguments. diff --git a/theories/Structures/OrdersEx.v b/theories/Structures/OrdersEx.v index b0702f6818..f8a08bf4e9 100644 --- a/theories/Structures/OrdersEx.v +++ b/theories/Structures/OrdersEx.v @@ -11,8 +11,6 @@ * Institution: LRI, CNRS UMR 8623 - Université Paris Sud * 91405 Orsay, France *) -(* $Id$ *) - Require Import Orders NPeano POrderedType NArith ZArith RelationPairs EqualitiesFacts. diff --git a/theories/Wellfounded/Disjoint_Union.v b/theories/Wellfounded/Disjoint_Union.v index 785d623b46..f856c86245 100644 --- a/theories/Wellfounded/Disjoint_Union.v +++ b/theories/Wellfounded/Disjoint_Union.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - (** Author: Cristina Cornes From : Constructing Recursion Operators in Type Theory L. Paulson JSC (1986) 2, 325-355 *) diff --git a/theories/Wellfounded/Inclusion.v b/theories/Wellfounded/Inclusion.v index 01049989e3..4d7139a512 100644 --- a/theories/Wellfounded/Inclusion.v +++ b/theories/Wellfounded/Inclusion.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - (** Author: Bruno Barras *) Require Import Relation_Definitions. diff --git a/theories/Wellfounded/Inverse_Image.v b/theories/Wellfounded/Inverse_Image.v index c57e707259..6f7a310d57 100644 --- a/theories/Wellfounded/Inverse_Image.v +++ b/theories/Wellfounded/Inverse_Image.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - (** Author: Bruno Barras *) Section Inverse_Image. diff --git a/theories/Wellfounded/Lexicographic_Exponentiation.v b/theories/Wellfounded/Lexicographic_Exponentiation.v index ff18890005..378b471847 100644 --- a/theories/Wellfounded/Lexicographic_Exponentiation.v +++ b/theories/Wellfounded/Lexicographic_Exponentiation.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - (** Author: Cristina Cornes From : Constructing Recursion Operators in Type Theory diff --git a/theories/Wellfounded/Lexicographic_Product.v b/theories/Wellfounded/Lexicographic_Product.v index 5144c0bee7..e52c3acae4 100644 --- a/theories/Wellfounded/Lexicographic_Product.v +++ b/theories/Wellfounded/Lexicographic_Product.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - (** Authors: Bruno Barras, Cristina Cornes *) Require Import Eqdep. diff --git a/theories/Wellfounded/Transitive_Closure.v b/theories/Wellfounded/Transitive_Closure.v index c999b58eee..a6092fe377 100644 --- a/theories/Wellfounded/Transitive_Closure.v +++ b/theories/Wellfounded/Transitive_Closure.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - (** Author: Bruno Barras *) Require Import Relation_Definitions. diff --git a/theories/Wellfounded/Union.v b/theories/Wellfounded/Union.v index fbb3d9e3c9..dbc36e3b12 100644 --- a/theories/Wellfounded/Union.v +++ b/theories/Wellfounded/Union.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - (** Author: Bruno Barras *) Require Import Relation_Operators. diff --git a/theories/Wellfounded/Well_Ordering.v b/theories/Wellfounded/Well_Ordering.v index e11b892484..8a5bf57f0a 100644 --- a/theories/Wellfounded/Well_Ordering.v +++ b/theories/Wellfounded/Well_Ordering.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - (** Author: Cristina Cornes. From: Constructing Recursion Operators in Type Theory L. Paulson JSC (1986) 2, 325-355 *) diff --git a/theories/Wellfounded/Wellfounded.v b/theories/Wellfounded/Wellfounded.v index fe05d61eda..77c676fc69 100644 --- a/theories/Wellfounded/Wellfounded.v +++ b/theories/Wellfounded/Wellfounded.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - Require Export Disjoint_Union. Require Export Inclusion. Require Export Inverse_Image. diff --git a/theories/ZArith/BinInt.v b/theories/ZArith/BinInt.v index 2807532caa..06adc620fd 100644 --- a/theories/ZArith/BinInt.v +++ b/theories/ZArith/BinInt.v @@ -7,8 +7,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - (***********************************************************) (** Binary Integers (Pierre Crégut, CNET, Lannion, France) *) (***********************************************************) diff --git a/theories/ZArith/Int.v b/theories/ZArith/Int.v index 30c08fdc12..3a0d7090d6 100644 --- a/theories/ZArith/Int.v +++ b/theories/ZArith/Int.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) -(* $Id$ *) - (** * An light axiomatization of integers (used in FSetAVL). *) (** We define a signature for an integer datatype based on [Z]. diff --git a/theories/ZArith/Wf_Z.v b/theories/ZArith/Wf_Z.v index 46f64c88db..7bbab9aaf4 100644 --- a/theories/ZArith/Wf_Z.v +++ b/theories/ZArith/Wf_Z.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - Require Import BinInt. Require Import Zcompare. Require Import Zorder. diff --git a/theories/ZArith/ZArith.v b/theories/ZArith/ZArith.v index 7a68bd5113..dba123091c 100644 --- a/theories/ZArith/ZArith.v +++ b/theories/ZArith/ZArith.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - (** Library for manipulating integers based on binary encoding *) Require Export ZArith_base. diff --git a/theories/ZArith/ZArith_base.v b/theories/ZArith/ZArith_base.v index cd866c375c..ac86f50f6e 100644 --- a/theories/ZArith/ZArith_base.v +++ b/theories/ZArith/ZArith_base.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) - (** Library for manipulating integers based on binary encoding. These are the basic modules, required by [Omega] and [Ring] for instance. The full library is [ZArith]. *) diff --git a/theories/ZArith/ZArith_dec.v b/theories/ZArith/ZArith_dec.v index 6e69350db7..2dce5fbe4a 100644 --- a/theories/ZArith/ZArith_dec.v +++ b/theories/ZArith/ZArith_dec.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - Require Import Sumbool. Require Import BinInt. diff --git a/theories/ZArith/Zabs.v b/theories/ZArith/Zabs.v index ba454c327a..517973a1e3 100644 --- a/theories/ZArith/Zabs.v +++ b/theories/ZArith/Zabs.v @@ -6,8 +6,6 @@ (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - (** Binary Integers (Pierre Crégut (CNET, Lannion, France) *) Require Import Arith_base. diff --git a/theories/ZArith/Zbool.v b/theories/ZArith/Zbool.v index 8cdd73cc7c..61d706b23b 100644 --- a/theories/ZArith/Zbool.v +++ b/theories/ZArith/Zbool.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) - Require Import BinInt. Require Import Zeven. Require Import Zorder. diff --git a/theories/ZArith/Zcomplements.v b/theories/ZArith/Zcomplements.v index 08cc564de5..103c2c9d5a 100644 --- a/theories/ZArith/Zcomplements.v +++ b/theories/ZArith/Zcomplements.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - Require Import ZArithRing. Require Import ZArith_base. Require Export Omega. diff --git a/theories/ZArith/Zdigits.v b/theories/ZArith/Zdigits.v index 0a6c94986a..f30d46cf34 100644 --- a/theories/ZArith/Zdigits.v +++ b/theories/ZArith/Zdigits.v @@ -7,8 +7,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - (** Bit vectors interpreted as integers. Contribution by Jean Duprat (ENS Lyon). *) diff --git a/theories/ZArith/Zdiv.v b/theories/ZArith/Zdiv.v index 66e275b61b..0cd5bed864 100644 --- a/theories/ZArith/Zdiv.v +++ b/theories/ZArith/Zdiv.v @@ -7,8 +7,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - (* Contribution by Claude Marché and Xavier Urbain *) (** Euclidean Division diff --git a/theories/ZArith/Zeven.v b/theories/ZArith/Zeven.v index 091310439d..4dfce35cec 100644 --- a/theories/ZArith/Zeven.v +++ b/theories/ZArith/Zeven.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - Require Import BinInt. Open Scope Z_scope. diff --git a/theories/ZArith/Zgcd_alt.v b/theories/ZArith/Zgcd_alt.v index 447f6101a7..f65a8f53bf 100644 --- a/theories/ZArith/Zgcd_alt.v +++ b/theories/ZArith/Zgcd_alt.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - (** * Zgcd_alt : an alternate version of Zgcd, based on Euler's algorithm *) (** diff --git a/theories/ZArith/Zhints.v b/theories/ZArith/Zhints.v index 5459e693df..d3d3eff0d4 100644 --- a/theories/ZArith/Zhints.v +++ b/theories/ZArith/Zhints.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - (** This file centralizes the lemmas about [Z], classifying them according to the way they can be used in automatic search *) diff --git a/theories/ZArith/Zlogarithm.v b/theories/ZArith/Zlogarithm.v index 70a959c2a3..397a8ab93d 100644 --- a/theories/ZArith/Zlogarithm.v +++ b/theories/ZArith/Zlogarithm.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - (**********************************************************************) (** The integer logarithms with base 2. diff --git a/theories/ZArith/Zmax.v b/theories/ZArith/Zmax.v index 1d9b1f108d..b9ff036aa9 100644 --- a/theories/ZArith/Zmax.v +++ b/theories/ZArith/Zmax.v @@ -5,8 +5,6 @@ (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - (** THIS FILE IS DEPRECATED. Use [ZBinary.Z] instead. *) Require Export BinInt Zcompare Zorder ZBinary. diff --git a/theories/ZArith/Zmin.v b/theories/ZArith/Zmin.v index e1599d9438..317f912eb1 100644 --- a/theories/ZArith/Zmin.v +++ b/theories/ZArith/Zmin.v @@ -5,8 +5,6 @@ (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - (** THIS FILE IS DEPRECATED. Use [ZBinary.Z] instead. *) Require Import BinInt Zcompare Zorder ZBinary. diff --git a/theories/ZArith/Zmisc.v b/theories/ZArith/Zmisc.v index 178ae5f158..820ed4a69d 100644 --- a/theories/ZArith/Zmisc.v +++ b/theories/ZArith/Zmisc.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - Require Import Wf_nat. Require Import BinInt. Require Import Zcompare. diff --git a/theories/ZArith/Znat.v b/theories/ZArith/Znat.v index dfd9b54506..1ca476d354 100644 --- a/theories/ZArith/Znat.v +++ b/theories/ZArith/Znat.v @@ -7,8 +7,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - (** Binary Integers (Pierre Crégut, CNET, Lannion, France) *) Require Export Arith_base. diff --git a/theories/ZArith/Znumtheory.v b/theories/ZArith/Znumtheory.v index 2a2751c9db..82ea3e94ad 100644 --- a/theories/ZArith/Znumtheory.v +++ b/theories/ZArith/Znumtheory.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - Require Import ZArith_base. Require Import ZArithRing. Require Import Zcomplements. diff --git a/theories/ZArith/Zorder.v b/theories/ZArith/Zorder.v index 511c364bc7..d2c8d9c04f 100644 --- a/theories/ZArith/Zorder.v +++ b/theories/ZArith/Zorder.v @@ -6,8 +6,6 @@ (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - (** Binary Integers (Pierre Crégut, CNET, Lannion, France) *) Require Import BinPos. diff --git a/theories/ZArith/Zpow_facts.v b/theories/ZArith/Zpow_facts.v index 1d9b3dfc97..43190ed055 100644 --- a/theories/ZArith/Zpow_facts.v +++ b/theories/ZArith/Zpow_facts.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - Require Import ZArith_base. Require Import ZArithRing. Require Import Zcomplements. diff --git a/theories/ZArith/Zpower.v b/theories/ZArith/Zpower.v index 508e6601c4..ad02acb23a 100644 --- a/theories/ZArith/Zpower.v +++ b/theories/ZArith/Zpower.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - Require Import Wf_nat. Require Import ZArith_base. Require Export Zpow_def. diff --git a/theories/ZArith/Zsqrt.v b/theories/ZArith/Zsqrt.v index b845cf47a2..79714114bb 100644 --- a/theories/ZArith/Zsqrt.v +++ b/theories/ZArith/Zsqrt.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) - Require Import ZArithRing. Require Import Omega. Require Export ZArith_base. diff --git a/theories/ZArith/Zwf.v b/theories/ZArith/Zwf.v index 32d6de19a4..88a5a9a56b 100644 --- a/theories/ZArith/Zwf.v +++ b/theories/ZArith/Zwf.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) - Require Import ZArith_base. Require Export Wf_nat. Require Import Omega. diff --git a/theories/ZArith/auxiliary.v b/theories/ZArith/auxiliary.v index 7af99ece96..81584e1e35 100644 --- a/theories/ZArith/auxiliary.v +++ b/theories/ZArith/auxiliary.v @@ -7,8 +7,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - (** Binary Integers (Pierre Crégut, CNET, Lannion, France) *) Require Export Arith_base. |