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 /ide | |
| 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 'ide')
| -rw-r--r-- | ide/command_windows.ml | 2 | ||||
| -rw-r--r-- | ide/command_windows.mli | 2 | ||||
| -rw-r--r-- | ide/config_lexer.mll | 2 | ||||
| -rw-r--r-- | ide/config_parser.mly | 2 | ||||
| -rw-r--r-- | ide/coq.ml | 2 | ||||
| -rw-r--r-- | ide/coq.mli | 2 | ||||
| -rw-r--r-- | ide/coq_commands.ml | 2 | ||||
| -rw-r--r-- | ide/coq_lex.mll | 2 | ||||
| -rw-r--r-- | ide/coq_tactics.ml | 2 | ||||
| -rw-r--r-- | ide/coq_tactics.mli | 2 | ||||
| -rw-r--r-- | ide/coqide.ml | 2 | ||||
| -rw-r--r-- | ide/coqide.mli | 2 | ||||
| -rw-r--r-- | ide/gtk_parsing.ml | 2 | ||||
| -rw-r--r-- | ide/highlight.mll | 2 | ||||
| -rw-r--r-- | ide/ideproof.ml | 2 | ||||
| -rw-r--r-- | ide/ideutils.ml | 2 | ||||
| -rw-r--r-- | ide/ideutils.mli | 2 | ||||
| -rw-r--r-- | ide/preferences.ml | 2 | ||||
| -rw-r--r-- | ide/preferences.mli | 2 | ||||
| -rw-r--r-- | ide/tags.ml | 2 | ||||
| -rw-r--r-- | ide/typed_notebook.ml | 2 | ||||
| -rw-r--r-- | ide/undo.ml | 2 | ||||
| -rw-r--r-- | ide/undo_lablgtk_ge212.mli | 2 | ||||
| -rw-r--r-- | ide/undo_lablgtk_ge26.mli | 2 | ||||
| -rw-r--r-- | ide/undo_lablgtk_lt26.mli | 2 | ||||
| -rw-r--r-- | ide/utf8_convert.mll | 2 | ||||
| -rw-r--r-- | ide/utils/config_file.ml | 2 |
27 files changed, 0 insertions, 54 deletions
diff --git a/ide/command_windows.ml b/ide/command_windows.ml index f6ef42221c..92dcd82220 100644 --- a/ide/command_windows.ml +++ b/ide/command_windows.ml @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) - class command_window () = (* let window = GWindow.window ~allow_grow:true ~allow_shrink:true diff --git a/ide/command_windows.mli b/ide/command_windows.mli index 4104f086c2..b211afabdc 100644 --- a/ide/command_windows.mli +++ b/ide/command_windows.mli @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - class command_window : unit -> object diff --git a/ide/config_lexer.mll b/ide/config_lexer.mll index 97aeb2f5a4..cafa96e43d 100644 --- a/ide/config_lexer.mll +++ b/ide/config_lexer.mll @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) - { open Lexing diff --git a/ide/config_parser.mly b/ide/config_parser.mly index bd5577db30..104d31f3c8 100644 --- a/ide/config_parser.mly +++ b/ide/config_parser.mly @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************/ -/* $Id$ */ - %{ open Parsing diff --git a/ide/coq.ml b/ide/coq.ml index 9b0afc7bed..383a7a34c9 100644 --- a/ide/coq.ml +++ b/ide/coq.ml @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) - open Vernac open Vernacexpr open Pfedit diff --git a/ide/coq.mli b/ide/coq.mli index d30f7168f9..d1568203fc 100644 --- a/ide/coq.mli +++ b/ide/coq.mli @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - open Names open Term open Environ diff --git a/ide/coq_commands.ml b/ide/coq_commands.ml index e4a3ae56a5..1d56489df1 100644 --- a/ide/coq_commands.ml +++ b/ide/coq_commands.ml @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) - let commands = [ [(* "Abort"; *) "Add Abstract Ring A Aplus Amult Aone Azero Ainv Aeq T."; diff --git a/ide/coq_lex.mll b/ide/coq_lex.mll index 36b567b734..ea981d7b75 100644 --- a/ide/coq_lex.mll +++ b/ide/coq_lex.mll @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) - { open Lexing diff --git a/ide/coq_tactics.ml b/ide/coq_tactics.ml index c6e1f1a448..307ee2522c 100644 --- a/ide/coq_tactics.ml +++ b/ide/coq_tactics.ml @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) - let tactics = [ "Abstract"; "Absurd"; diff --git a/ide/coq_tactics.mli b/ide/coq_tactics.mli index c31933baad..41219fdf6a 100644 --- a/ide/coq_tactics.mli +++ b/ide/coq_tactics.mli @@ -6,7 +6,5 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - val tactics : string list diff --git a/ide/coqide.ml b/ide/coqide.ml index 8dc4867568..32f2bdd711 100644 --- a/ide/coqide.ml +++ b/ide/coqide.ml @@ -7,8 +7,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) - open Preferences open Vernacexpr open Coq diff --git a/ide/coqide.mli b/ide/coqide.mli index 4c01e747a1..f91ce01840 100644 --- a/ide/coqide.mli +++ b/ide/coqide.mli @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - (* The CoqIde main module. The following function [start] will parse the command line, initialize the load path, load the input state, load the files given on the command line, load the ressource file, diff --git a/ide/gtk_parsing.ml b/ide/gtk_parsing.ml index e92a345e33..5411499ca4 100644 --- a/ide/gtk_parsing.ml +++ b/ide/gtk_parsing.ml @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: coqide.ml 11952 2009-03-02 15:29:08Z vgross $ *) - open Ideutils diff --git a/ide/highlight.mll b/ide/highlight.mll index 3acdd4f086..0a623ca384 100644 --- a/ide/highlight.mll +++ b/ide/highlight.mll @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) - { open Lexing diff --git a/ide/ideproof.ml b/ide/ideproof.ml index 700b5a7295..3d86f52c62 100644 --- a/ide/ideproof.ml +++ b/ide/ideproof.ml @@ -7,8 +7,6 @@ (************************************************************************) -(* $Id$ *) - (* tag is the tag to be hooked, item is the item covered by this tag, make_menu * * is the template for building menu if needed, sel_cb is the callback if * there diff --git a/ide/ideutils.ml b/ide/ideutils.ml index 14e803899c..aaade8aa5a 100644 --- a/ide/ideutils.ml +++ b/ide/ideutils.ml @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) - open Preferences diff --git a/ide/ideutils.mli b/ide/ideutils.mli index fbd5af44ea..0d57b855e2 100644 --- a/ide/ideutils.mli +++ b/ide/ideutils.mli @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - val async : ('a -> unit) -> 'a -> unit val sync : ('a -> 'b) -> 'a -> 'b diff --git a/ide/preferences.ml b/ide/preferences.ml index 4e87d1df44..b8eb07cc5a 100644 --- a/ide/preferences.ml +++ b/ide/preferences.ml @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) - open Configwin open Printf open Util diff --git a/ide/preferences.mli b/ide/preferences.mli index 6ee7918fed..cd955d7bd8 100644 --- a/ide/preferences.mli +++ b/ide/preferences.mli @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - type pref = { mutable cmd_coqc : string; diff --git a/ide/tags.ml b/ide/tags.ml index 842ac53bc5..3b407a19d4 100644 --- a/ide/tags.ml +++ b/ide/tags.ml @@ -7,8 +7,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) - let make_tag (tt:GText.tag_table) ~name prop = let new_tag = GText.tag ~name () in diff --git a/ide/typed_notebook.ml b/ide/typed_notebook.ml index cadb5941e4..bd26bab273 100644 --- a/ide/typed_notebook.ml +++ b/ide/typed_notebook.ml @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: coqide.ml 11952 2009-03-02 15:29:08Z vgross $ *) - class ['a] typed_notebook default_build nb = object(self) inherit GPack.notebook nb as super diff --git a/ide/undo.ml b/ide/undo.ml index 18c2f7a4da..56b8196bbb 100644 --- a/ide/undo.ml +++ b/ide/undo.ml @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) - open GText open Ideutils type action = diff --git a/ide/undo_lablgtk_ge212.mli b/ide/undo_lablgtk_ge212.mli index 32717fa8e4..d7c12de8e2 100644 --- a/ide/undo_lablgtk_ge212.mli +++ b/ide/undo_lablgtk_ge212.mli @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: undo_lablgtk_ge26.mli 7580 2005-11-18 17:09:10Z herbelin $ i*) - (* An undoable view class *) class undoable_view : [> Gtk.text_view] Gtk.obj -> diff --git a/ide/undo_lablgtk_ge26.mli b/ide/undo_lablgtk_ge26.mli index 52bd67215c..ab51a66b21 100644 --- a/ide/undo_lablgtk_ge26.mli +++ b/ide/undo_lablgtk_ge26.mli @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - (* An undoable view class *) class undoable_view : [> Gtk.text_view] Gtk.obj -> diff --git a/ide/undo_lablgtk_lt26.mli b/ide/undo_lablgtk_lt26.mli index 46ecfb1d7c..330accc7b5 100644 --- a/ide/undo_lablgtk_lt26.mli +++ b/ide/undo_lablgtk_lt26.mli @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - (* An undoable view class *) class undoable_view : Gtk.text_view Gtk.obj -> diff --git a/ide/utf8_convert.mll b/ide/utf8_convert.mll index 82b3053479..b1eb0f4c24 100644 --- a/ide/utf8_convert.mll +++ b/ide/utf8_convert.mll @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) - { open Lexing let b = Buffer.create 127 diff --git a/ide/utils/config_file.ml b/ide/utils/config_file.ml index 37f2e9a4a3..921d3d9c90 100644 --- a/ide/utils/config_file.ml +++ b/ide/utils/config_file.ml @@ -23,8 +23,6 @@ (* *) (*********************************************************************************) -(* $Id$ *) - (* TODO *) (* section comments *) (* better obsoletes: no "{}", line cuts *) |
