diff options
| author | letouzey | 2010-04-29 13:50:31 +0000 |
|---|---|---|
| committer | letouzey | 2010-04-29 13:50:31 +0000 |
| commit | af93e4cf8b1a839d21499b3b9737bb8904edcae8 (patch) | |
| tree | b9a4f28e6f8106bcf19e017f64147f836f810c4b /theories/MSets | |
| 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/MSets')
| -rw-r--r-- | theories/MSets/MSetAVL.v | 2 | ||||
| -rw-r--r-- | theories/MSets/MSetDecide.v | 2 | ||||
| -rw-r--r-- | theories/MSets/MSetEqProperties.v | 2 | ||||
| -rw-r--r-- | theories/MSets/MSetFacts.v | 2 | ||||
| -rw-r--r-- | theories/MSets/MSetInterface.v | 2 | ||||
| -rw-r--r-- | theories/MSets/MSetList.v | 2 | ||||
| -rw-r--r-- | theories/MSets/MSetProperties.v | 2 | ||||
| -rw-r--r-- | theories/MSets/MSetToFiniteSet.v | 2 | ||||
| -rw-r--r-- | theories/MSets/MSetWeakList.v | 2 | ||||
| -rw-r--r-- | theories/MSets/MSets.v | 2 |
10 files changed, 0 insertions, 20 deletions
diff --git a/theories/MSets/MSetAVL.v b/theories/MSets/MSetAVL.v index f79f8d0b26..0d24e0339e 100644 --- a/theories/MSets/MSetAVL.v +++ b/theories/MSets/MSetAVL.v @@ -7,8 +7,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) -(* $Id$ *) - (** * MSetAVL : Implementation of MSetInterface via AVL trees *) (** This module implements finite sets using AVL trees. diff --git a/theories/MSets/MSetDecide.v b/theories/MSets/MSetDecide.v index 884ed42353..1161739ed9 100644 --- a/theories/MSets/MSetDecide.v +++ b/theories/MSets/MSetDecide.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) -(* $Id$ *) - (**************************************************************) (* MSetDecide.v *) (* *) diff --git a/theories/MSets/MSetEqProperties.v b/theories/MSets/MSetEqProperties.v index fe6c3c79c2..2e7da404e8 100644 --- a/theories/MSets/MSetEqProperties.v +++ b/theories/MSets/MSetEqProperties.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) -(* $Id$ *) - (** * Finite sets library *) (** This module proves many properties of finite sets that diff --git a/theories/MSets/MSetFacts.v b/theories/MSets/MSetFacts.v index 84f6a17055..b61bf3fe79 100644 --- a/theories/MSets/MSetFacts.v +++ b/theories/MSets/MSetFacts.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) -(* $Id$ *) - (** * Finite sets library *) (** This functor derives additional facts from [MSetInterface.S]. These diff --git a/theories/MSets/MSetInterface.v b/theories/MSets/MSetInterface.v index 10776a5909..7dc3c96a86 100644 --- a/theories/MSets/MSetInterface.v +++ b/theories/MSets/MSetInterface.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) -(* $Id$ *) - (** * Finite set library *) (** Set interfaces, inspired by the one of Ocaml. When compared with diff --git a/theories/MSets/MSetList.v b/theories/MSets/MSetList.v index 0414e6eda9..b73af8f1ab 100644 --- a/theories/MSets/MSetList.v +++ b/theories/MSets/MSetList.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) -(* $Id$ *) - (** * Finite sets library *) (** This file proposes an implementation of the non-dependant diff --git a/theories/MSets/MSetProperties.v b/theories/MSets/MSetProperties.v index a9ba0a823b..14fe097a93 100644 --- a/theories/MSets/MSetProperties.v +++ b/theories/MSets/MSetProperties.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) -(* $Id$ *) - (** * Finite sets library *) (** This functor derives additional properties from [MSetInterface.S]. diff --git a/theories/MSets/MSetToFiniteSet.v b/theories/MSets/MSetToFiniteSet.v index f0b964cf2d..e8087bc572 100644 --- a/theories/MSets/MSetToFiniteSet.v +++ b/theories/MSets/MSetToFiniteSet.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) -(* $Id$ *) - (** * Finite sets library : conversion to old [Finite_sets] *) Require Import Ensembles Finite_sets. diff --git a/theories/MSets/MSetWeakList.v b/theories/MSets/MSetWeakList.v index 6b9c170790..8239ecef8b 100644 --- a/theories/MSets/MSetWeakList.v +++ b/theories/MSets/MSetWeakList.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) -(* $Id$ *) - (** * Finite sets library *) (** This file proposes an implementation of the non-dependant diff --git a/theories/MSets/MSets.v b/theories/MSets/MSets.v index 558b09562d..a4b9efc3bc 100644 --- a/theories/MSets/MSets.v +++ b/theories/MSets/MSets.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) -(* $Id$ *) - Require Export Orders. Require Export OrdersEx. Require Export OrdersAlt. |
