18 files changed, 0 insertions, 32 deletions
diff --git a/doc/refman/Extraction.tex b/doc/refman/Extraction.tex
index cfc9434139..277e3d5398 100644
--- a/doc/refman/Extraction.tex
+++ b/doc/refman/Extraction.tex
@@ -684,8 +684,6 @@ of the sources of \Coq.
  After compilation those two examples run nonetheless,
  thanks to the correction of the extraction~\cite{Let02}. 
 
-% $Id$ 
-
 %%% Local Variables: 
 %%% mode: latex
 %%% TeX-master: "Reference-Manual"
diff --git a/doc/refman/RefMan-add.tex b/doc/refman/RefMan-add.tex
index 52746fad6e..2094c9d2d5 100644
--- a/doc/refman/RefMan-add.tex
+++ b/doc/refman/RefMan-add.tex
@@ -51,8 +51,6 @@ can be found in the document {\tt Polynom.dvi}
 %anomalous behavior, please check first whether it has been already
 %reported in this document.
 
-% $Id$ 
-
 
 %%% Local Variables: 
 %%% mode: latex
diff --git a/doc/refman/RefMan-cic.tex b/doc/refman/RefMan-cic.tex
index f50c4fe1f0..4d473d54b6 100644
--- a/doc/refman/RefMan-cic.tex
+++ b/doc/refman/RefMan-cic.tex
@@ -1706,8 +1706,6 @@ impredicative system for sort \Set{} become~:
      
 
 
-% $Id$ 
-
 %%% Local Variables: 
 %%% mode: latex
 %%% TeX-master: "Reference-Manual"
diff --git a/doc/refman/RefMan-coi.tex b/doc/refman/RefMan-coi.tex
index 2c03966421..619a8ee104 100644
--- a/doc/refman/RefMan-coi.tex
+++ b/doc/refman/RefMan-coi.tex
@@ -403,4 +403,3 @@ See \cite{Gimenez95b} for a complete description about this development.
 
 %\end{document}
 
-% $Id$ 
diff --git a/doc/refman/RefMan-com.tex b/doc/refman/RefMan-com.tex
index cf47742859..824943d47d 100644
--- a/doc/refman/RefMan-com.tex
+++ b/doc/refman/RefMan-com.tex
@@ -376,8 +376,6 @@ makes more disk access. It is also less secure since an attacker might
 have replaced the compiled library $A$ after it has been read by the
 first command, but before it has been read by the second command.
 
-% $Id$ 
-
 %%% Local Variables: 
 %%% mode: latex
 %%% TeX-master: "Reference-Manual"
diff --git a/doc/refman/RefMan-gal.tex b/doc/refman/RefMan-gal.tex
index 9741061643..5461779feb 100644
--- a/doc/refman/RefMan-gal.tex
+++ b/doc/refman/RefMan-gal.tex
@@ -1657,4 +1657,3 @@ To be able to unfold a proof, you should end the proof by {\tt Defined}
 % TeX-master: "Reference-Manual"
 % End: 
 
-% $Id$ 
diff --git a/doc/refman/RefMan-ide.tex b/doc/refman/RefMan-ide.tex
index 831eb9d08c..c00a389f46 100644
--- a/doc/refman/RefMan-ide.tex
+++ b/doc/refman/RefMan-ide.tex
@@ -312,8 +312,6 @@ or
 
     
 
-% $Id$ 
-
 %%% Local Variables: 
 %%% mode: latex
 %%% TeX-master: "Reference-Manual"
diff --git a/doc/refman/RefMan-ind.tex b/doc/refman/RefMan-ind.tex
index 23006b72e1..959442402e 100644
--- a/doc/refman/RefMan-ind.tex
+++ b/doc/refman/RefMan-ind.tex
@@ -508,4 +508,3 @@ Check tree_forest_mutind.
 
 %\end{document}
 
-% $Id$ 
diff --git a/doc/refman/RefMan-int.tex b/doc/refman/RefMan-int.tex
index c40224a485..6d2c37f75b 100644
--- a/doc/refman/RefMan-int.tex
+++ b/doc/refman/RefMan-int.tex
@@ -140,8 +140,6 @@ is given in the additional document {\tt Library.ps}.
 \end{description}
 
 
-% $Id$ 
-
 %%% Local Variables: 
 %%% mode: latex
 %%% TeX-master: "Reference-Manual"
diff --git a/doc/refman/RefMan-lib.tex b/doc/refman/RefMan-lib.tex
index 99c25d0568..7caf6126ec 100644
--- a/doc/refman/RefMan-lib.tex
+++ b/doc/refman/RefMan-lib.tex
@@ -1095,8 +1095,6 @@ description, etc.) and the possibility to download them one by one.
 You will also find informations on how to submit a new
 contribution.
 
-% $Id$ 
-
 %%% Local Variables: 
 %%% mode: latex
 %%% TeX-master: "Reference-Manual"
diff --git a/doc/refman/RefMan-modr.tex b/doc/refman/RefMan-modr.tex
index 05bc3496ea..9ab8aded9c 100644
--- a/doc/refman/RefMan-modr.tex
+++ b/doc/refman/RefMan-modr.tex
@@ -556,8 +556,6 @@ In the rules below we assume $\Gamma_P$ is $[p_1:P_1;\ldots;p_r:P_r]$,
 % \end{itemize}
 
 
-% $Id$
-
 %%% Local Variables: 
 %%% mode: latex
 %%% TeX-master: "Reference-Manual"
diff --git a/doc/refman/RefMan-oth.tex b/doc/refman/RefMan-oth.tex
index 9e18d0af26..b765ef7d4f 100644
--- a/doc/refman/RefMan-oth.tex
+++ b/doc/refman/RefMan-oth.tex
@@ -1121,8 +1121,6 @@ control the scope of their effect. There are four kinds of commands:
 \end{itemize}
 
 
-% $Id$ 
-
 %%% Local Variables: 
 %%% mode: latex
 %%% TeX-master: "Reference-Manual"
diff --git a/doc/refman/RefMan-pre.tex b/doc/refman/RefMan-pre.tex
index 1b6efc582c..736627122b 100644
--- a/doc/refman/RefMan-pre.tex
+++ b/doc/refman/RefMan-pre.tex
@@ -698,8 +698,6 @@ Hugo Herbelin\\
 % Integration of ZArith lemmas from Sophia and Nijmegen.
 
 
-% $Id$ 
-
 %%% Local Variables: 
 %%% mode: latex
 %%% TeX-master: "Reference-Manual"
diff --git a/doc/refman/RefMan-pro.tex b/doc/refman/RefMan-pro.tex
index 593ed771f8..a8bb7966a0 100644
--- a/doc/refman/RefMan-pro.tex
+++ b/doc/refman/RefMan-pro.tex
@@ -402,8 +402,6 @@ All the hypotheses remains usable in the proof development.
 This command goes back to the default mode which is to print all
 available hypotheses.
 
-% $Id$
-
 %%% Local Variables: 
 %%% mode: latex
 %%% TeX-master: "Reference-Manual"
diff --git a/doc/refman/RefMan-syn.tex b/doc/refman/RefMan-syn.tex
index 548c259856..6b471ec392 100644
--- a/doc/refman/RefMan-syn.tex
+++ b/doc/refman/RefMan-syn.tex
@@ -1101,8 +1101,6 @@ places where a list of the underlying entry can be used: {\nterm{entry}} is
 either {\tt\small constr}, {\tt\small hyp}, {\tt\small integer} or
 {\tt\small int\_or\_var}.
 
-% $Id$ 
-
 %%% Local Variables: 
 %%% mode: latex
 %%% TeX-master: "Reference-Manual"
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index 139f80cf3c..0e6bff9db5 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -4257,8 +4257,6 @@ Chapter~\ref{TacticLanguage} gives examples of more complex
 user-defined tactics.
 
 
-% $Id$ 
-
 %%% Local Variables: 
 %%% mode: latex
 %%% TeX-master: "Reference-Manual"
diff --git a/doc/refman/RefMan-uti.tex b/doc/refman/RefMan-uti.tex
index f1dde04ad4..996a15cd40 100644
--- a/doc/refman/RefMan-uti.tex
+++ b/doc/refman/RefMan-uti.tex
@@ -264,8 +264,6 @@ There are man pages for the commands {\tt coqdep}, {\tt gallina} and
 \RefManCutCommand{ENDREFMAN=\thepage}
 %END LATEX
 
-% $Id$
-
 %%% Local Variables: 
 %%% mode: latex
 %%% TeX-master: t
diff --git a/doc/refman/Reference-Manual.tex b/doc/refman/Reference-Manual.tex
index 946bfda12e..0c90e61ba5 100644
--- a/doc/refman/Reference-Manual.tex
+++ b/doc/refman/Reference-Manual.tex
@@ -138,4 +138,3 @@ Options A and B of the licence are {\em not} elected.}
 \end{document}
 
 
-% $Id$