aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/FSets
diff options
context:
space:
mode:
authorGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2010-04-29 13:50:31 +0000
committerGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2010-04-29 13:50:31 +0000
commitaf93e4cf8b1a839d21499b3b9737bb8904edcae8 (patch)
treeb9a4f28e6f8106bcf19e017f64147f836f810c4b /theories/FSets
parent0f61b02f84b41e1f019cd78824de28f18ff854aa (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/FSets')
-rw-r--r--theories/FSets/FMapAVL.v2
-rw-r--r--theories/FSets/FMapFacts.v2
-rw-r--r--theories/FSets/FMapFullAVL.v2
-rw-r--r--theories/FSets/FMapInterface.v2
-rw-r--r--theories/FSets/FMapList.v2
-rw-r--r--theories/FSets/FMapPositive.v2
-rw-r--r--theories/FSets/FMapWeakList.v2
-rw-r--r--theories/FSets/FMaps.v2
-rw-r--r--theories/FSets/FSetAVL.v2
-rw-r--r--theories/FSets/FSetBridge.v2
-rw-r--r--theories/FSets/FSetDecide.v2
-rw-r--r--theories/FSets/FSetEqProperties.v2
-rw-r--r--theories/FSets/FSetFacts.v2
-rw-r--r--theories/FSets/FSetInterface.v2
-rw-r--r--theories/FSets/FSetList.v2
-rw-r--r--theories/FSets/FSetProperties.v2
-rw-r--r--theories/FSets/FSetToFiniteSet.v2
-rw-r--r--theories/FSets/FSetWeakList.v2
-rw-r--r--theories/FSets/FSets.v2
19 files changed, 0 insertions, 38 deletions
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.