Imported Upstream version 8.3.pl3upstream/8.3.pl3

26 files changed, 91 insertions, 79 deletions

diff --git a/ide/command_windows.ml b/ide/command_windows.ml
index 4510189b..1df83803 100644
--- a/ide/command_windows.ml
+++ b/ide/command_windows.ml
@@ -1,12 +1,12 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: command_windows.ml 13323 2010-07-24 15:57:30Z herbelin $ *)
+(* $Id: command_windows.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
 
 class command_window () =
 (*  let window = GWindow.window
diff --git a/ide/command_windows.mli b/ide/command_windows.mli
index eb0aa568..0f5c208b 100644
--- a/ide/command_windows.mli
+++ b/ide/command_windows.mli
@@ -1,12 +1,12 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: command_windows.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: command_windows.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
 
 class command_window :
   unit ->
diff --git a/ide/config_lexer.mll b/ide/config_lexer.mll
index 4e3ffd89..3724f2bf 100644
--- a/ide/config_lexer.mll
+++ b/ide/config_lexer.mll
@@ -1,12 +1,12 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: config_lexer.mll 13323 2010-07-24 15:57:30Z herbelin $ *)
+(* $Id: config_lexer.mll 14641 2011-11-06 11:59:10Z herbelin $ *)
 
 {
 
diff --git a/ide/config_parser.mly b/ide/config_parser.mly
index 0859cbe0..d49e22eb 100644
--- a/ide/config_parser.mly
+++ b/ide/config_parser.mly
@@ -1,12 +1,12 @@
 /************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************/
 
-/* $Id: config_parser.mly 13323 2010-07-24 15:57:30Z herbelin $ */
+/* $Id: config_parser.mly 14641 2011-11-06 11:59:10Z herbelin $ */
 
 %{
 
diff --git a/ide/coq.ml b/ide/coq.ml
index bb08e2af..1c6229b4 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -1,12 +1,12 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: coq.ml 13751 2010-12-24 09:56:05Z letouzey $ *)
+(* $Id: coq.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
 
 open Vernac
 open Vernacexpr
@@ -297,7 +297,7 @@ let rec attribute_of_vernac_command = function
   (* Proof management *)
   | VernacGoal _ -> [GoalStartingCommand]
 
-  | VernacAbort _ -> [NavigationCommand]
+  | VernacAbort _ -> []
   | VernacAbortAll -> [NavigationCommand]
   | VernacRestart -> [NavigationCommand]
   | VernacSuspend -> [NavigationCommand]
diff --git a/ide/coq.mli b/ide/coq.mli
index af17c0e9..9dec52c6 100644
--- a/ide/coq.mli
+++ b/ide/coq.mli
@@ -1,12 +1,12 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: coq.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: coq.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
 
 open Names
 open Term
diff --git a/ide/coq_commands.ml b/ide/coq_commands.ml
index c8a5c940..d41bcf29 100644
--- a/ide/coq_commands.ml
+++ b/ide/coq_commands.ml
@@ -1,12 +1,12 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: coq_commands.ml 13323 2010-07-24 15:57:30Z herbelin $ *)
+(* $Id: coq_commands.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
 
 let commands = [
   [(* "Abort"; *)
diff --git a/ide/coq_lex.mll b/ide/coq_lex.mll
index 5bff10b3..02e21166 100644
--- a/ide/coq_lex.mll
+++ b/ide/coq_lex.mll
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -67,7 +67,7 @@
   let is_proof_end =
     let h = Hashtbl.create 97 in
     List.iter (fun s -> Hashtbl.add h s ())
-      [ "Qed" ; "Defined" ; "Admitted" ];
+      [ "Qed" ; "Defined" ; "Admitted"; "Abort" ];
     Hashtbl.mem h
 
   let start = ref true
diff --git a/ide/coq_tactics.ml b/ide/coq_tactics.ml
index e3d8131e..568594bd 100644
--- a/ide/coq_tactics.ml
+++ b/ide/coq_tactics.ml
@@ -1,12 +1,12 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: coq_tactics.ml 13323 2010-07-24 15:57:30Z herbelin $ *)
+(* $Id: coq_tactics.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
 
 let tactics = [
   "Abstract";
diff --git a/ide/coq_tactics.mli b/ide/coq_tactics.mli
index e33c73ab..4c583d3a 100644
--- a/ide/coq_tactics.mli
+++ b/ide/coq_tactics.mli
@@ -1,12 +1,12 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: coq_tactics.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: coq_tactics.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
 
 val tactics : string list
 
diff --git a/ide/coqide.ml b/ide/coqide.ml
index ce4f0666..162728ad 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -1,12 +1,12 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: coqide.ml 13751 2010-12-24 09:56:05Z letouzey $ *)
+(* $Id: coqide.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
 
 open Preferences
 open Vernacexpr
@@ -306,7 +306,8 @@ let remove_current_view_page () =
       kill_input_view c
   in
   let current = session_notebook#current_term in
-    if current.script#buffer#modified then
+    if not current.script#buffer#modified then do_remove ()
+    else
       match GToolbox.question_box ~title:"Close"
               ~buttons:["Save Buffer and Close";
                         "Close without Saving";
@@ -1680,34 +1681,42 @@ let choose_save session =
     save_dialog#show ()
  *)
 
+(* Nota: using && here has the advantage of working both under win32 and unix.
+   If someday we want the main command to be tried even if the "cd" has failed,
+   then we should use " ; " under unix but " & " under win32 (cf. #2363).
+*)
+
+let local_cd file =
+  "cd " ^ Filename.quote (Filename.dirname file) ^ " && "
+
 let do_print session =
   let av = session.analyzed_view in
-    if session.filename = ""
-    then flash_info "Cannot print: this buffer has no name"
-    else begin
-      let cmd =
-        "cd " ^ Filename.quote (Filename.dirname session.filename) ^ "; " ^
-        !current.cmd_coqdoc ^ " -ps " ^ Filename.quote (Filename.basename session.filename) ^
-        " | " ^ !current.cmd_print
-      in
-      let print_window = GWindow.window ~title:"Print" ~modal:true ~position:`CENTER ~wm_class:"CoqIDE" ~wm_name: "CoqIDE"  () in
-      let vbox_print = GPack.vbox ~spacing:10 ~border_width:10 ~packing:print_window#add () in
-      let _ = GMisc.label ~justify:`LEFT ~text:"Print using the following command:" ~packing:vbox_print#add () in
-      let print_entry = GEdit.entry ~text:cmd ~editable:true ~width_chars:80 ~packing:vbox_print#add () in
-      let hbox_print = GPack.hbox ~spacing:10 ~packing:vbox_print#add () in
-      let print_cancel_button = GButton.button ~stock:`CANCEL ~label:"Cancel" ~packing:hbox_print#add () in
-      let print_button  = GButton.button ~stock:`PRINT  ~label:"Print"  ~packing:hbox_print#add () in
-      let callback_print () =
-        let cmd = print_entry#text in
-        let s,_ = run_command av#insert_message cmd in
-          flash_info (cmd ^ if s = Unix.WEXITED 0 then " succeeded" else " failed");
-          print_window#destroy ()
-      in
-        ignore (print_cancel_button#connect#clicked ~callback:print_window#destroy) ;
-        ignore (print_button#connect#clicked ~callback:callback_print);
-        print_window#misc#show ()
-    end
-
+    match av#filename with
+      |None -> flash_info "Cannot print: this buffer has no name"
+      |Some f_name -> begin
+	  let cmd =
+	local_cd session.filename ^
+              !current.cmd_coqdoc ^ " --coqlib_path " ^ Envars.coqlib () ^
+	      " -ps " ^ Filename.quote (Filename.basename f_name) ^
+              " | " ^ !current.cmd_print
+	  in
+	  let print_window = GWindow.window ~title:"Print" ~modal:true ~position:`CENTER ~wm_class:"CoqIDE" ~wm_name: "CoqIDE"  () in
+	  let vbox_print = GPack.vbox ~spacing:10 ~border_width:10 ~packing:print_window#add () in
+	  let _ = GMisc.label ~justify:`LEFT ~text:"Print using the following command:" ~packing:vbox_print#add () in
+	  let print_entry = GEdit.entry ~text:cmd ~editable:true ~width_chars:80 ~packing:vbox_print#add () in
+	  let hbox_print = GPack.hbox ~spacing:10 ~packing:vbox_print#add () in
+	  let print_cancel_button = GButton.button ~stock:`CANCEL ~label:"Cancel" ~packing:hbox_print#add () in
+	  let print_button  = GButton.button ~stock:`PRINT  ~label:"Print"  ~packing:hbox_print#add () in
+	  let callback_print () =
+            let cmd = print_entry#text in
+            let s,_ = run_command av#insert_message cmd in
+              flash_info (cmd ^ if s = Unix.WEXITED 0 then " succeeded" else " failed");
+              print_window#destroy ()
+	  in
+            ignore (print_cancel_button#connect#clicked ~callback:print_window#destroy) ;
+            ignore (print_button#connect#clicked ~callback:callback_print);
+            print_window#misc#show ()
+	end
 
 let main files =
   (* Statup preferences *)
@@ -1956,8 +1965,11 @@ let main files =
 				  | _ -> assert false
 			    in
 			    let cmd =
-			      "cd " ^ Filename.quote (Filename.dirname f) ^ "; " ^
-				!current.cmd_coqdoc ^ " --" ^ kind ^ " -o " ^ (Filename.quote output) ^ " " ^ (Filename.quote basef)
+			      local_cd f ^
+				!current.cmd_coqdoc ^ " --coqlib_path " ^
+				Envars.coqlib () ^ " --" ^ kind ^
+				" -o " ^ (Filename.quote output) ^ " " ^
+				(Filename.quote basef)
 			    in
 			    let s,_ = run_command av#insert_message cmd in
 			      flash_info (cmd ^
@@ -2862,7 +2874,7 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S);
 						    flash_info "Cannot make: this buffer has no name"
 						| Some f ->
 						    let cmd =
-						      "cd " ^ Filename.quote (Filename.dirname f) ^ "; " ^ !current.cmd_make in
+						      local_cd f ^ !current.cmd_make in
 
 						      (*
 							save_f ();
@@ -2929,7 +2941,7 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S);
 						    flash_info "Cannot make makefile: this buffer has no name"
 						| Some f ->
 						    let cmd =
-						      "cd " ^ Filename.quote (Filename.dirname f) ^ "; " ^ !current.cmd_coqmakefile in
+						      local_cd f ^ !current.cmd_coqmakefile in
 						    let s,res = run_command av#insert_message cmd in
 						      flash_info
 							(!current.cmd_coqmakefile ^ if s = Unix.WEXITED 0 then " succeeded" else " failed")
diff --git a/ide/coqide.mli b/ide/coqide.mli
index b70a9b4b..ea995c71 100644
--- a/ide/coqide.mli
+++ b/ide/coqide.mli
@@ -1,12 +1,12 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: coqide.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: coqide.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
 
 (* The CoqIde main module. The following function [start] will parse the
    command line, initialize the load path, load the input
diff --git a/ide/gtk_parsing.ml b/ide/gtk_parsing.ml
index ddf4a754..1b52dba3 100644
--- a/ide/gtk_parsing.ml
+++ b/ide/gtk_parsing.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/ide/highlight.mll b/ide/highlight.mll
index dfcc4354..c288d6a3 100644
--- a/ide/highlight.mll
+++ b/ide/highlight.mll
@@ -1,12 +1,12 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: highlight.mll 13323 2010-07-24 15:57:30Z herbelin $ *)
+(* $Id: highlight.mll 14641 2011-11-06 11:59:10Z herbelin $ *)
 
 {
 
diff --git a/ide/ideutils.ml b/ide/ideutils.ml
index 8b7840e3..a6be77f2 100644
--- a/ide/ideutils.ml
+++ b/ide/ideutils.ml
@@ -1,12 +1,12 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: ideutils.ml 13751 2010-12-24 09:56:05Z letouzey $ *)
+(* $Id: ideutils.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
 
 
 open Preferences
diff --git a/ide/ideutils.mli b/ide/ideutils.mli
index ade460c6..d6311c78 100644
--- a/ide/ideutils.mli
+++ b/ide/ideutils.mli
@@ -1,12 +1,12 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: ideutils.mli 13751 2010-12-24 09:56:05Z letouzey $ i*)
+(*i $Id: ideutils.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
 
 val async : ('a -> unit) -> 'a -> unit
 val sync  : ('a -> 'b) -> 'a -> 'b
diff --git a/ide/preferences.ml b/ide/preferences.ml
index 5d97f659..790bf560 100644
--- a/ide/preferences.ml
+++ b/ide/preferences.ml
@@ -1,12 +1,12 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: preferences.ml 13436 2010-09-19 10:18:18Z herbelin $ *)
+(* $Id: preferences.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
 
 open Configwin
 open Printf
diff --git a/ide/preferences.mli b/ide/preferences.mli
index 50659717..472ae30f 100644
--- a/ide/preferences.mli
+++ b/ide/preferences.mli
@@ -1,12 +1,12 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: preferences.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: preferences.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
 
 type pref =
     {
diff --git a/ide/tags.ml b/ide/tags.ml
index f6ffcde4..aacac46e 100644
--- a/ide/tags.ml
+++ b/ide/tags.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/ide/typed_notebook.ml b/ide/typed_notebook.ml
index e674212c..3dd2279f 100644
--- a/ide/typed_notebook.ml
+++ b/ide/typed_notebook.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/ide/uim/coqide-rules.scm b/ide/uim/coqide-rules.scm
index c483c88b..af25b613 100644
--- a/ide/uim/coqide-rules.scm
+++ b/ide/uim/coqide-rules.scm
@@ -1,6 +1,6 @@
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;;  v      ;   The Coq Proof Assistant  /  The Coq Development Team     ;;
-;; <O___,, ;   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     ;;
+;; <O___,, ;   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     ;;
 ;;   \VV/  ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;;    //   ;      This file is distributed under the terms of the       ;;
 ;;         ;       GNU Lesser General Public License Version 2.1        ;;
diff --git a/ide/undo.ml b/ide/undo.ml
index 819b4807..55d0f288 100644
--- a/ide/undo.ml
+++ b/ide/undo.ml
@@ -1,12 +1,12 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: undo.ml 13323 2010-07-24 15:57:30Z herbelin $ *)
+(* $Id: undo.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
 
 open GText
 open Ideutils
diff --git a/ide/undo_lablgtk_ge212.mli b/ide/undo_lablgtk_ge212.mli
index 6cc4757b..1326a486 100644
--- a/ide/undo_lablgtk_ge212.mli
+++ b/ide/undo_lablgtk_ge212.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/ide/undo_lablgtk_ge26.mli b/ide/undo_lablgtk_ge26.mli
index c260f171..698b34c5 100644
--- a/ide/undo_lablgtk_ge26.mli
+++ b/ide/undo_lablgtk_ge26.mli
@@ -1,12 +1,12 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: undo_lablgtk_ge26.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: undo_lablgtk_ge26.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
 
 (* An undoable view class *)
 
diff --git a/ide/undo_lablgtk_lt26.mli b/ide/undo_lablgtk_lt26.mli
index c9d1bacb..e99d3141 100644
--- a/ide/undo_lablgtk_lt26.mli
+++ b/ide/undo_lablgtk_lt26.mli
@@ -1,12 +1,12 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: undo_lablgtk_lt26.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: undo_lablgtk_lt26.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
 
 (* An undoable view class *)
 
diff --git a/ide/utf8_convert.mll b/ide/utf8_convert.mll
index 5034ab3c..ce0c4836 100644
--- a/ide/utf8_convert.mll
+++ b/ide/utf8_convert.mll
@@ -1,12 +1,12 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: utf8_convert.mll 13323 2010-07-24 15:57:30Z herbelin $ *)
+(* $Id: utf8_convert.mll 14641 2011-11-06 11:59:10Z herbelin $ *)
 
 {
   open Lexing