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

22 files changed, 0 insertions, 37 deletions

diff --git a/doc/common/macros.tex b/doc/common/macros.tex
index 6048a75fdb..c4e7973636 100755
--- a/doc/common/macros.tex
+++ b/doc/common/macros.tex
@@ -520,8 +520,6 @@
         {\begin{center}\begin{rulebox}}
         {\end{rulebox}\end{center}}
 
-% $Id$ 
-
 
 %%% Local Variables: 
 %%% mode: latex
diff --git a/doc/common/title.tex b/doc/common/title.tex
index abd106ea40..1dc524324e 100755
--- a/doc/common/title.tex
+++ b/doc/common/title.tex
@@ -70,4 +70,3 @@ V\coqversion, \today
 % TeX-master: ""
 % End: 
 
-% $Id$ 
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$ 
diff --git a/doc/stdlib/Library.tex b/doc/stdlib/Library.tex
index f5509c3a3c..02dc61bfe4 100755
--- a/doc/stdlib/Library.tex
+++ b/doc/stdlib/Library.tex
@@ -61,4 +61,3 @@ you can access from the \Coq\ home page at
 
 \end{document}
 
-% $Id$ 
diff --git a/doc/tutorial/Tutorial.tex b/doc/tutorial/Tutorial.tex
index 219706e35d..43c8bf620b 100755
--- a/doc/tutorial/Tutorial.tex
+++ b/doc/tutorial/Tutorial.tex
@@ -1574,4 +1574,3 @@ with \Coq, in order to acquaint yourself with various proof techniques.
 
 \end{document}
 
-% $Id$