9 files changed, 0 insertions, 18 deletions
diff --git a/theories/Program/Basics.v b/theories/Program/Basics.v
index 0a4b15d29d..69e3206ba4 100644
--- a/theories/Program/Basics.v
+++ b/theories/Program/Basics.v
@@ -6,8 +6,6 @@
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
-(* $Id$ *)
-
 (** Standard functions and combinators.
 
    Proofs about them require functional extensionality and can be found
diff --git a/theories/Program/Combinators.v b/theories/Program/Combinators.v
index 31661b9d37..8d041422d8 100644
--- a/theories/Program/Combinators.v
+++ b/theories/Program/Combinators.v
@@ -6,8 +6,6 @@
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
-(* $Id$ *)
-
 (** * Proofs about standard combinators, exports functional extensionality.
 
    Author: Matthieu Sozeau
diff --git a/theories/Program/Equality.v b/theories/Program/Equality.v
index c3c5f9c95e..5a047ec5ce 100644
--- a/theories/Program/Equality.v
+++ b/theories/Program/Equality.v
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
-
 (** Tactics related to (dependent) equality and proof irrelevance. *)
 
 Require Export ProofIrrelevance.
diff --git a/theories/Program/Program.v b/theories/Program/Program.v
index cdfc785837..ffdd1bd55b 100644
--- a/theories/Program/Program.v
+++ b/theories/Program/Program.v
@@ -5,8 +5,6 @@
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
-(* $Id$ *)
-
 Require Export Coq.Program.Utils.
 Require Export Coq.Program.Wf.
 Require Export Coq.Program.Equality.
diff --git a/theories/Program/Subset.v b/theories/Program/Subset.v
index 89f477d8f9..523171013b 100644
--- a/theories/Program/Subset.v
+++ b/theories/Program/Subset.v
@@ -5,8 +5,6 @@
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
-(* $Id$ *)
-
 (** Tactics related to subsets and proof irrelevance. *)
 
 Require Import Coq.Program.Utils.
diff --git a/theories/Program/Syntax.v b/theories/Program/Syntax.v
index 916c33ee62..2c5fb79c56 100644
--- a/theories/Program/Syntax.v
+++ b/theories/Program/Syntax.v
@@ -5,8 +5,6 @@
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
-(* $Id$ *)
-
 (** Custom notations and implicits for Coq prelude definitions.
 
    Author: Matthieu Sozeau
diff --git a/theories/Program/Tactics.v b/theories/Program/Tactics.v
index d187941d20..f4d53c2791 100644
--- a/theories/Program/Tactics.v
+++ b/theories/Program/Tactics.v
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
-
 (** This module implements various tactics used to simplify the goals produced by Program,
    which are also generally useful. *)
 
diff --git a/theories/Program/Utils.v b/theories/Program/Utils.v
index fbf0b03cf8..dbcaea80fd 100644
--- a/theories/Program/Utils.v
+++ b/theories/Program/Utils.v
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
-
 (** Various syntaxic shortands that are useful with [Program]. *)
 
 Require Export Coq.Program.Tactics.
diff --git a/theories/Program/Wf.v b/theories/Program/Wf.v
index c4d06fd722..70a6fe97a4 100644
--- a/theories/Program/Wf.v
+++ b/theories/Program/Wf.v
@@ -5,8 +5,6 @@
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
-(* $Id$ *)
-
 (** Reformulation of the Wf module using subsets where possible, providing
    the support for [Program]'s treatment of well-founded definitions. *)