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 /parsing | |
| 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 'parsing')
38 files changed, 0 insertions, 76 deletions
diff --git a/parsing/argextend.ml4 b/parsing/argextend.ml4 index 89edbb1230..3b2160af18 100644 --- a/parsing/argextend.ml4 +++ b/parsing/argextend.ml4 @@ -8,8 +8,6 @@ (*i camlp4use: "pa_extend.cmo q_MLast.cmo" i*) -(* $Id$ *) - open Genarg open Q_util open Q_coqast diff --git a/parsing/egrammar.ml b/parsing/egrammar.ml index b5ee1ae60c..337ddd7ed4 100644 --- a/parsing/egrammar.ml +++ b/parsing/egrammar.ml @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) - open Pp open Util open Pcoq diff --git a/parsing/egrammar.mli b/parsing/egrammar.mli index 50132fd385..1e9159933d 100644 --- a/parsing/egrammar.mli +++ b/parsing/egrammar.mli @@ -6,8 +6,6 @@ * GNU Lesser General Public License Version 2.1 ***********************************************************************) -(*i $Id$ i*) - open Util open Names open Topconstr diff --git a/parsing/extend.ml b/parsing/extend.ml index 7643120f3c..a3ef4893a1 100644 --- a/parsing/extend.ml +++ b/parsing/extend.ml @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - open Util (**********************************************************************) diff --git a/parsing/extend.mli b/parsing/extend.mli index 6bf8165ebd..5ff475f79b 100644 --- a/parsing/extend.mli +++ b/parsing/extend.mli @@ -6,8 +6,6 @@ * GNU Lesser General Public License Version 2.1 ***********************************************************************) -(*i $Id$ i*) - open Util (********************************************************************* diff --git a/parsing/extrawit.ml b/parsing/extrawit.ml index 122730f72e..7ccff54359 100644 --- a/parsing/extrawit.ml +++ b/parsing/extrawit.ml @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - open Util open Genarg diff --git a/parsing/extrawit.mli b/parsing/extrawit.mli index f15c388b6c..b330a8e64a 100644 --- a/parsing/extrawit.mli +++ b/parsing/extrawit.mli @@ -6,8 +6,6 @@ * GNU Lesser General Public License Version 2.1 ***********************************************************************) -(*i $Id$ i*) - open Util open Genarg open Tacexpr diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4 index 393125e29e..4329033774 100644 --- a/parsing/g_constr.ml4 +++ b/parsing/g_constr.ml4 @@ -8,8 +8,6 @@ (*i camlp4use: "pa_extend.cmo" i*) -(* $Id$ *) - open Pp open Pcoq open Constr diff --git a/parsing/g_ltac.ml4 b/parsing/g_ltac.ml4 index 0e97b2a7fd..ca9e90cd54 100644 --- a/parsing/g_ltac.ml4 +++ b/parsing/g_ltac.ml4 @@ -8,8 +8,6 @@ (*i camlp4use: "pa_extend.cmo" i*) -(* $Id$ *) - open Pp open Util open Topconstr diff --git a/parsing/g_natsyntax.mli b/parsing/g_natsyntax.mli index 20f5c1bfd1..3751f603b4 100644 --- a/parsing/g_natsyntax.mli +++ b/parsing/g_natsyntax.mli @@ -6,8 +6,6 @@ * GNU Lesser General Public License Version 2.1 ***********************************************************************) -(*i $Id$ i*) - (** Nice syntax for naturals. *) open Notation diff --git a/parsing/g_prim.ml4 b/parsing/g_prim.ml4 index 6e7acd3f59..02b3df3fb8 100644 --- a/parsing/g_prim.ml4 +++ b/parsing/g_prim.ml4 @@ -8,8 +8,6 @@ (*i camlp4use: "pa_extend.cmo" i*) -(*i $Id$ i*) - open Pcoq open Names open Libnames diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4 index 27ad1e9645..758d4599aa 100644 --- a/parsing/g_proofs.ml4 +++ b/parsing/g_proofs.ml4 @@ -8,8 +8,6 @@ (*i camlp4use: "pa_extend.cmo" i*) -(* $Id$ *) - open Pcoq open Pp diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4 index c845daf2ca..0ef18de2fd 100644 --- a/parsing/g_tactic.ml4 +++ b/parsing/g_tactic.ml4 @@ -8,8 +8,6 @@ (*i camlp4use: "pa_extend.cmo" i*) -(* $Id$ *) - open Pp open Pcoq open Util diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index db683b9a91..29b51322d2 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -9,8 +9,6 @@ (*i camlp4deps: "parsing/grammar.cma" i*) (*i camlp4use: "pa_extend.cmo" i*) -(* $Id$ *) - open Pp open Util diff --git a/parsing/g_xml.ml4 b/parsing/g_xml.ml4 index 0f70290419..8bda1e58f1 100644 --- a/parsing/g_xml.ml4 +++ b/parsing/g_xml.ml4 @@ -8,8 +8,6 @@ (*i camlp4use: "pa_extend.cmo" i*) -(* $Id$ *) - open Pp open Util open Names diff --git a/parsing/g_zsyntax.mli b/parsing/g_zsyntax.mli index c4f39f80b0..29dd60f353 100644 --- a/parsing/g_zsyntax.mli +++ b/parsing/g_zsyntax.mli @@ -6,6 +6,4 @@ * GNU Lesser General Public License Version 2.1 ***********************************************************************) -(*i $Id$ i*) - (** Nice syntax for integers. *) diff --git a/parsing/lexer.ml4 b/parsing/lexer.ml4 index 4b15e200ca..afb26ec81e 100644 --- a/parsing/lexer.ml4 +++ b/parsing/lexer.ml4 @@ -8,8 +8,6 @@ (*i camlp4use: "pa_macro.cmo" i*) -(*i $Id$ i*) - open Pp open Util open Token diff --git a/parsing/lexer.mli b/parsing/lexer.mli index aabac79fb7..09492ceb11 100644 --- a/parsing/lexer.mli +++ b/parsing/lexer.mli @@ -6,8 +6,6 @@ * GNU Lesser General Public License Version 2.1 ***********************************************************************) -(*i $Id$ i*) - open Pp open Util diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4 index de15d8a7cb..e11cdd96ff 100644 --- a/parsing/pcoq.ml4 +++ b/parsing/pcoq.ml4 @@ -8,8 +8,6 @@ (*i camlp4use: "pa_extend.cmo pa_macro.cmo" i*) -(*i $Id$ i*) - open Pp open Util open Names diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index f9e65acacc..23d85d94a8 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -6,8 +6,6 @@ * GNU Lesser General Public License Version 2.1 ***********************************************************************) -(*i $Id$ i*) - open Util open Names open Rawterm diff --git a/parsing/ppconstr.ml b/parsing/ppconstr.ml index 08ac7fd684..597505686d 100644 --- a/parsing/ppconstr.ml +++ b/parsing/ppconstr.ml @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) - (*i*) open Util open Pp diff --git a/parsing/ppconstr.mli b/parsing/ppconstr.mli index d2d44f245c..2becdbcfd6 100644 --- a/parsing/ppconstr.mli +++ b/parsing/ppconstr.mli @@ -7,8 +7,6 @@ * GNU Lesser General Public License Version 2.1 ***********************************************************************) -(*i $Id$ i*) - open Pp open Environ open Term diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml index 5f02daf4a0..9714b7fa95 100644 --- a/parsing/pptactic.ml +++ b/parsing/pptactic.ml @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) - open Pp open Names open Namegen diff --git a/parsing/pptactic.mli b/parsing/pptactic.mli index a6eacd53a9..34a7089fef 100644 --- a/parsing/pptactic.mli +++ b/parsing/pptactic.mli @@ -6,8 +6,6 @@ * GNU Lesser General Public License Version 2.1 ***********************************************************************) -(*i $Id$ i*) - open Pp open Genarg open Tacexpr diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml index 470f937c00..99039e8672 100644 --- a/parsing/ppvernac.ml +++ b/parsing/ppvernac.ml @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) - open Pp open Names open Nameops diff --git a/parsing/ppvernac.mli b/parsing/ppvernac.mli index 6c2916f412..98511f3e5e 100644 --- a/parsing/ppvernac.mli +++ b/parsing/ppvernac.mli @@ -6,8 +6,6 @@ * GNU Lesser General Public License Version 2.1 ***********************************************************************) -(*i $Id$ i*) - open Pp open Genarg open Vernacexpr diff --git a/parsing/prettyp.ml b/parsing/prettyp.ml index 98c93f897a..882a94ffbb 100644 --- a/parsing/prettyp.ml +++ b/parsing/prettyp.ml @@ -10,8 +10,6 @@ * on May-June 2006 for implementation of abstraction of pretty-printing of objects. *) -(* $Id$ *) - open Pp open Util open Names diff --git a/parsing/prettyp.mli b/parsing/prettyp.mli index 04aad9ab42..913ab8b433 100644 --- a/parsing/prettyp.mli +++ b/parsing/prettyp.mli @@ -6,8 +6,6 @@ * GNU Lesser General Public License Version 2.1 ***********************************************************************) -(*i $Id$ i*) - open Pp open Util open Names diff --git a/parsing/printer.ml b/parsing/printer.ml index cd07c4e15c..d3c4ae63da 100644 --- a/parsing/printer.ml +++ b/parsing/printer.ml @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) - open Pp open Util open Names diff --git a/parsing/printer.mli b/parsing/printer.mli index 6289fa66a7..5cd402e9f3 100644 --- a/parsing/printer.mli +++ b/parsing/printer.mli @@ -6,8 +6,6 @@ * GNU Lesser General Public License Version 2.1 ***********************************************************************) -(*i $Id$ i*) - open Pp open Names open Libnames diff --git a/parsing/q_constr.ml4 b/parsing/q_constr.ml4 index 093910b4d4..28911794fd 100644 --- a/parsing/q_constr.ml4 +++ b/parsing/q_constr.ml4 @@ -8,8 +8,6 @@ (*i camlp4use: "pa_extend.cmo q_MLast.cmo" i*) -(* $Id$ *) - open Rawterm open Term open Names diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4 index 1bd5af5336..89a1c2ed5f 100644 --- a/parsing/q_coqast.ml4 +++ b/parsing/q_coqast.ml4 @@ -8,8 +8,6 @@ (*i camlp4use: "q_MLast.cmo pa_macro.cmo" i*) -(* $Id$ *) - open Util open Names open Libnames diff --git a/parsing/q_util.ml4 b/parsing/q_util.ml4 index 7b9037d92d..e5851f81d8 100644 --- a/parsing/q_util.ml4 +++ b/parsing/q_util.ml4 @@ -8,8 +8,6 @@ (*i camlp4use: "q_MLast.cmo" i*) -(* $Id$ *) - (* This file defines standard combinators to build ml expressions *) open Util diff --git a/parsing/q_util.mli b/parsing/q_util.mli index 4fe853702a..59b3f334cc 100644 --- a/parsing/q_util.mli +++ b/parsing/q_util.mli @@ -6,8 +6,6 @@ * GNU Lesser General Public License Version 2.1 ***********************************************************************) -(*i $Id$ i*) - val patt_of_expr : MLast.expr -> MLast.patt val mlexpr_of_list : ('a -> MLast.expr) -> 'a list -> MLast.expr diff --git a/parsing/tacextend.ml4 b/parsing/tacextend.ml4 index 517e34aa2c..f77b24eff3 100644 --- a/parsing/tacextend.ml4 +++ b/parsing/tacextend.ml4 @@ -8,8 +8,6 @@ (*i camlp4use: "pa_extend.cmo q_MLast.cmo" i*) -(* $Id$ *) - open Util open Genarg open Q_util diff --git a/parsing/tactic_printer.ml b/parsing/tactic_printer.ml index bf554acf69..57af218524 100644 --- a/parsing/tactic_printer.ml +++ b/parsing/tactic_printer.ml @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) - open Pp open Util open Sign diff --git a/parsing/tactic_printer.mli b/parsing/tactic_printer.mli index 836c4712ba..129f0e6719 100644 --- a/parsing/tactic_printer.mli +++ b/parsing/tactic_printer.mli @@ -6,8 +6,6 @@ * GNU Lesser General Public License Version 2.1 ***********************************************************************) -(*i $Id$ i*) - open Pp open Sign open Evd diff --git a/parsing/vernacextend.ml4 b/parsing/vernacextend.ml4 index e1997b878b..ff354d5e08 100644 --- a/parsing/vernacextend.ml4 +++ b/parsing/vernacextend.ml4 @@ -8,8 +8,6 @@ (*i camlp4use: "pa_extend.cmo q_MLast.cmo" i*) -(* $Id$ *) - open Util open Genarg open Q_util |