aboutsummaryrefslogtreecommitdiffhomepage
path: root/ide
diff options
context:
space:
mode:
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 f6ef42221..92dcd8222 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 4104f086c..b211afabd 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 97aeb2f5a..cafa96e43 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 bd5577db3..104d31f3c 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 9b0afc7be..383a7a34c 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 d30f7168f..d1568203f 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 e4a3ae56a..1d56489df 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 36b567b73..ea981d7b7 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 c6e1f1a44..307ee2522 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 c31933baa..41219fdf6 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 8dc486756..32f2bdd71 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 4c01e747a..f91ce0184 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 e92a345e3..5411499ca 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 3acdd4f08..0a623ca38 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 700b5a729..3d86f52c6 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 14e803899..aaade8aa5 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 fbd5af44e..0d57b855e 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 4e87d1df4..b8eb07cc5 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 6ee7918fe..cd955d7bd 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 842ac53bc..3b407a19d 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 cadb5941e..bd26bab27 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 18c2f7a4d..56b8196bb 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 32717fa8e..d7c12de8e 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 52bd67215..ab51a66b2 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 46ecfb1d7..330accc7b 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 82b305347..b1eb0f4c2 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 37f2e9a4a..921d3d9c9 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 *)
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-26 22:40:38 +0000