aboutsummaryrefslogtreecommitdiff
path: root/ide
diff options
context:
space:
mode:
authorletouzey2010-04-29 13:50:31 +0000
committerletouzey2010-04-29 13:50:31 +0000
commitaf93e4cf8b1a839d21499b3b9737bb8904edcae8 (patch)
treeb9a4f28e6f8106bcf19e017f64147f836f810c4b /ide
parent0f61b02f84b41e1f019cd78824de28f18ff854aa (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.ml2
-rw-r--r--ide/command_windows.mli2
-rw-r--r--ide/config_lexer.mll2
-rw-r--r--ide/config_parser.mly2
-rw-r--r--ide/coq.ml2
-rw-r--r--ide/coq.mli2
-rw-r--r--ide/coq_commands.ml2
-rw-r--r--ide/coq_lex.mll2
-rw-r--r--ide/coq_tactics.ml2
-rw-r--r--ide/coq_tactics.mli2
-rw-r--r--ide/coqide.ml2
-rw-r--r--ide/coqide.mli2
-rw-r--r--ide/gtk_parsing.ml2
-rw-r--r--ide/highlight.mll2
-rw-r--r--ide/ideproof.ml2
-rw-r--r--ide/ideutils.ml2
-rw-r--r--ide/ideutils.mli2
-rw-r--r--ide/preferences.ml2
-rw-r--r--ide/preferences.mli2
-rw-r--r--ide/tags.ml2
-rw-r--r--ide/typed_notebook.ml2
-rw-r--r--ide/undo.ml2
-rw-r--r--ide/undo_lablgtk_ge212.mli2
-rw-r--r--ide/undo_lablgtk_ge26.mli2
-rw-r--r--ide/undo_lablgtk_lt26.mli2
-rw-r--r--ide/utf8_convert.mll2
-rw-r--r--ide/utils/config_file.ml2
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 *)