diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-04-29 13:50:31 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 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 18dbd27f9..0de9136fd 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 2d54f0e8d..9395fc56c 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 208c25789..b4cdb3c82 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 9fd59e103..d94a71c9e 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 0f2595b26..c401eb283 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 38d1aef0e..635b72671 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 999a64544..c717e9bf5 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 312b76e97..7d5b36ae5 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 f50dcc84d..f118eb85b 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 eaa1bb2d6..fa4414146 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 8c5315624..58631a987 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 70169f52a..20aad5c05 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 6140eeb5a..edf1e34d5 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 af435e54b..12819940d 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 b94cc2485..ffce72774 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 ba03a40bd..c980baf09 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 cd6c0a29e..490bf8e55 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 8346cae38..811068daf 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 42335f98b..d8b46c78f 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 9b7c62615..28613eecc 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 5bc5d2a58..c12a577f8 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 66ab6f1c8..a1ea2ebc8 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 625cbd194..9a2e738eb 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 d9da08672..b41d65c39 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 90f7ee662..799438d89 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 c2b5ed793..573916ddc 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 06ab77cfb..a34c49175 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 5e9d4afa6..fde053026 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 0a35ef45e..75c51a8dd 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 d0f243474..d62bd0674 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 f6e51018a..df288add4 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 4b827c244..2421c90d0 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 a8193ef3c..4c39964a9 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 c41c57698..36fe2b9a6 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 33b4350f8..ab2131185 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 669be8b0f..dbdff45f3 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 c6252de9c..e0ddbe3ab 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 4c59971cb..fd58ec10a 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 afac5af8c..1facce290 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 e60cca9d9..252e67930 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 56fc35d89..f15ab222c 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 56ad2ed11..e85cc283e 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 38ed172b8..6c1e8ca89 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 6b1102406..19b25d95a 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 bc6c731f6..df627a14b 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 1b1bae352..8d6ca420b 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 89cdc932f..a87103232 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 ec0c6a559..755bc7dd0 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 b750edfc0..f473b3342 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 8aede5527..a23263890 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 f83259c44..1f36306c3 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 84c26dacd..80da1c5d8 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 01138270e..3ac5d9e4a 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 711cbd9a6..2ea32e97c 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 eaa8f4034..9a7294119 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 092fce996..782ff6ca9 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 4fca1d1db..14832e0b7 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 1333f3545..ff6a18e14 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 0c628298d..9bf921b22 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 8779f2b45..045210d0a 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 45b949716..c8d809fd4 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 7141f26cb..6ff820299 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 6ccf8a022..66f90e18f 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 3209860f3..0a1a0f9b8 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 766456fff..d1e3f90b3 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 e6c3a435b..0ed3bbbb7 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 0a21a9e27..3a743dd47 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 d42e71e55..88ccdb126 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 3fa053b7f..39a2968f7 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 7ed9c519b..2d75f065f 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 5b2f5063b..b32456a9e 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 b2c4a049d..903081ce6 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 1c2b97ce7..4a01f3fae 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 b0301994b..92e48e6a9 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 2b9df6d97..a5d1babaa 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 cee55dc81..7de6ddab6 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 b22a3a874..a271c05bc 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 4a7bd2ccc..67b853be9 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 0b0c329be..afbb5e6df 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 b30308af5..45c487cf7 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 df732959f..ee6dd96f2 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 3b91afd02..b3053fa1d 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 6d22b1a9e..8077cabf7 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 c6d32d9be..75441584d 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 a8a56ae74..dd1d56b31 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 18f3181b6..b513bdf73 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 d433be944..7de0aa7fc 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 5c6b4e89f..14ab70b67 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 4689fb46c..9c20905c7 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 c7cb9b0d4..d4d05fe1a 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 bf29c63dd..5d6a4f7d6 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 3651c1b2f..94922525b 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 fc4555a4a..f17e403ed 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 49fa12224..9313e1073 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 f79f8d0b2..0d24e0339 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 884ed4235..1161739ed 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 fe6c3c79c..2e7da404e 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 84f6a1705..b61bf3fe7 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 10776a590..7dc3c96a8 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 0414e6eda..b73af8f1a 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 a9ba0a823..14fe097a9 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 f0b964cf2..e8087bc57 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 6b9c17079..8239ecef8 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 558b09562..a4b9efc3b 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 b289380fd..6b668df60 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 a5f99cc66..a7b2336c8 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 009e64fd0..7282fc758 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 9540aace7..c217ada11 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 b699b7428..a79cfac3d 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 92559ff67..dc37fa6c2 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 0016d035f..feabd3b16 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 0891dea21..fea12a1d4 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 08da68444..f11fb67b1 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 af30b0175..0403722cb 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 b68e89560..0796d9f49 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 aa798e1c7..81b2c9403 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 23c62740c..bf18c1753 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 49a4f950a..a640aaf7f 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 1ce1e81b0..ae806dd5e 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 136f96c04..1c4247231 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 3405b6f4d..1395caa33 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 6a2a34449..8b978172c 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 e2c623201..81df55bd4 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 a7e556713..a5610fe78 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 88cbb484f..da75219a5 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 e2e5b563f..ca73a9f00 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 cc224254f..9b4c25e2c 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 a9c499fb9..01002656d 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 da0be5e2a..a2ee248ab 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 5663408d1..123c40428 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 de12993f8..adc843264 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 9158a214d..46f7810ac 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 44bb02ecc..ca288e6b2 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 849bf6b40..fdb7c77f6 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 84d840ad2..4a87a54c8 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 99be58ebd..1952f4e2a 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 45662d3b6..76451da33 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 aa62ae76b..c0b8074b6 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 3196f11ea..41b1d6e69 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 bc1dadcd9..aa857f3ca 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 8b5624cdf..cafcc549e 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 ffa91706f..ab12e584b 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 bcecb6a8a..2c4797969 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 417463eba..121b33b00 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 9535cfdb4..37a174c48 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 97c122029..66e9c6ceb 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 ee7ee159f..7cfa62eab 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 18e3b9b92..9f587a1d0 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 eb06cae03..7afbee4a4 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 296bd095f..c97aa9f3a 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 7b64a6983..acc43fc17 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 14fa0bfde..bfbcc2c65 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 125b4f62c..cc7bfe031 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 9f0b54a6a..859641280 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 0ce04e54e..67bc80850 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 42016ab10..cd3d8f0a8 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 842f4bcf2..f26f56d0c 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 22eb2cb34..2302e8d35 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 47bf38cba..12dcd3258 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 a2162b137..29d1838c2 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 090c02ecf..9439e04f5 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 9fc9b290e..eed7cac18 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 cbbcdbff5..bd666bc8b 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 1df032ea3..7d3117fdb 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 5442a5626..20cb01b16 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 9772e6a1f..9177b8092 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 e8651d47c..ba592507b 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 80d434bab..491c33666 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 3f60cbf1a..55a6302aa 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 49a60916a..8cbd96c1f 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 32860cd31..5022c9ae6 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 10d0189a3..6466fc511 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 0a4b15d29..69e3206ba 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 31661b9d3..8d041422d 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 c3c5f9c95..5a047ec5c 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 cdfc78583..ffdd1bd55 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 89f477d8f..523171013 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 916c33ee6..2c5fb79c5 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 d187941d2..f4d53c279 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 fbf0b03cf..dbcaea80f 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 c4d06fd72..70a6fe97a 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 f7a28598e..fe1ff3674 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 609241d5e..111d2391a 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 34d6267e3..b26b828ca 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 fbfae55c3..524996c38 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 12e371ee9..15fea8516 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 27e3c4e02..4f16f5b8c 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 8c9e2dfa3..96ed046a6 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 ef75323e0..1b9be0795 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 cccc8ceec..9c29e26a3 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 f22ff5cb2..48324e8e8 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 0d34d22c5..d0df984a1 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 6ea0767d0..68a842c9f 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 6c08356a7..c5e2c0ed3 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 7a893c53c..d27e0ae4c 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 e037c77b5..0d41b5900 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 1c74f55a0..287057f0f 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 774a0bd5c..eba81ff9b 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 b33274af9..ca7cb8fea 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 4037e3dec..72bd62a69 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 74bcf7dcd..0d75a9dee 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 97793386d..80a5b87a8 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 6a33b8092..e9a224b97 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 2b6af10ec..7c4555605 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 545bd68b2..8cf56cd7b 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 57b2c7675..e530070b1 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 6460a9271..1cccb8848 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 2c43ee9b9..13232566f 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 500dd5295..53267174b 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 1516b3384..a0b10c891 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 1d44b3e73..04c00cb30 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 3b685cd8a..28da1c7c4 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 1ed3fb713..abf0b883f 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 9715414f5..1ed75cdb6 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 ab1c07474..8843c5e6e 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 7588020c5..2e1bd0797 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 27d5c49ef..de3250529 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 023cfc93c..ab6ed8b10 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 6413943a9..19ebcd3cb 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 d18213db4..de57a5af2 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 7371c8acf..668891369 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 8890cbb50..dceb98d45 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 9fd6e0088..abf817d7a 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 f9b1b890f..f783d1d82 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 3aaa7300a..e0f47364f 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 c7d1893be..f922e25f6 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 a4feed8f3..957466cbe 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 bb3df6bb8..4e3f4d089 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 1ed6b03c5..9e5122062 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 917592702..155577746 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 33c20355c..a8f12a6b3 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 5b55896b1..a086cfd46 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 4981d6fdf..582b6be75 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 fe2da8391..1cf0944c0 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 a7fddb473..33ea1adba 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 9588e4438..265dae9d4 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 cb53b5346..62d8d9f5f 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 5b731488b..f38e59e82 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 82647c837..642e7fc9e 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 dbfc85bb9..dcfadd566 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 5882f953c..90048e50d 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 51e54860d..322808f9b 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 4f336648b..3961b8b0c 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 1976b435c..cfb952632 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 c03c4b95f..4f676484a 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 39e0331d5..bdc44dd17 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 1c6df08a4..f1e20b10e 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 c5530e7ca..cf641253a 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 5f6860997..5fbfadd4c 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 0719365f1..294dbb0cd 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 8c69e6877..6d537f59b 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 0fa9c74a8..8843cadd6 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 019c25a55..11ac3b9e4 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 fdcc4150f..da4a35813 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 64c341bd3..313a18dcc 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 b63ec1d47..0ae11b4f6 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 15c1b665e..8fe9928b1 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 7216ae335..5b7aa24b7 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 4fe8f4f6a..195f454e5 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 f593031a0..25a121cb3 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 c323ca356..9ecb600a5 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 36d2150c3..8f881c363 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 76f7f1ec8..61f783957 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 85d0cffcc..eb3273959 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 fd83b0e0d..484245bc8 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 11ac85e84..3b1e7057d 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 3554901b9..6fd07160f 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 970db1827..991b38242 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 d8bf7dc3c..a2a0f4584 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 909c79838..41e7f0edf 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 4124ef983..c48d22d62 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 238013b85..5830fabe4 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 8e6aa6dce..6ad0b6ba0 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 203e212b6..5faaebe28 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 c3cd4f4a8..e861b9ce7 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 d87259eec..931e29bf8 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 5f8da6a4d..f05cc473b 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 1f90c06cf..ba01f3d4c 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 15f298218..c6bf9e119 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 2c72e30b1..79e817717 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 4407ead41..2c02f8ddd 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 3d4430b9e..0a6dba982 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 72fbe7968..6b9007fdd 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 23ae4c85a..b054496e9 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 a39f336a5..600eabf11 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 96daca5cd..d7bdfbf71 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 d86b02a15..85e7fb176 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 b0702f681..f8a08bf4e 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 785d623b4..f856c8624 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 01049989e..4d7139a51 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 c57e70725..6f7a310d5 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 ff1889000..378b47184 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 5144c0bee..e52c3acae 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 c999b58ee..a6092fe37 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 fbb3d9e3c..dbc36e3b1 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 e11b89248..8a5bf57f0 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 fe05d61ed..77c676fc6 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 2807532ca..06adc620f 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 30c08fdc1..3a0d7090d 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 46f64c88d..7bbab9aaf 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 7a68bd511..dba123091 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 cd866c375..ac86f50f6 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 6e69350db..2dce5fbe4 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 ba454c327..517973a1e 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 8cdd73cc7..61d706b23 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 08cc564de..103c2c9d5 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 0a6c94986..f30d46cf3 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 66e275b61..0cd5bed86 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 091310439..4dfce35ce 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 447f6101a..f65a8f53b 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 5459e693d..d3d3eff0d 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 70a959c2a..397a8ab93 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 1d9b1f108..b9ff036aa 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 e1599d943..317f912eb 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 178ae5f15..820ed4a69 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 dfd9b5450..1ca476d35 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 2a2751c9d..82ea3e94a 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 511c364bc..d2c8d9c04 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 1d9b3dfc9..43190ed05 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 508e6601c..ad02acb23 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 b845cf47a..79714114b 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 32d6de19a..88a5a9a56 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 7af99ece9..81584e1e3 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. |