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

9 files changed, 0 insertions, 18 deletions

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. *)