Imported Upstream version 8.4dfsgupstream/8.4dfsg

28 files changed, 447 insertions, 445 deletions

diff --git a/ide/command_windows.ml b/ide/command_windows.ml
index a34e5ebe..470bd5b4 100644
--- a/ide/command_windows.ml
+++ b/ide/command_windows.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-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/ide/command_windows.mli b/ide/command_windows.mli
index c34b6cf6..30e953be 100644
--- a/ide/command_windows.mli
+++ b/ide/command_windows.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-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/ide/config_lexer.mll b/ide/config_lexer.mll
index 57699c68..4d91a11a 100644
--- a/ide/config_lexer.mll
+++ b/ide/config_lexer.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-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/ide/coq.ml b/ide/coq.ml
index 76dc5650..8b1fa0a3 100644
--- a/ide/coq.ml
+++ b/ide/coq.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-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/ide/coq.mli b/ide/coq.mli
index 7f61521e..f25268ef 100644
--- a/ide/coq.mli
+++ b/ide/coq.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-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/ide/coq_commands.ml b/ide/coq_commands.ml
index 256426d2..26dbcb12 100644
--- a/ide/coq_commands.ml
+++ b/ide/coq_commands.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-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/ide/coq_lex.mll b/ide/coq_lex.mll
index c9a9a826..8a4aa91c 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-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/ide/coqide.ml b/ide/coqide.ml
index 61280fd9..1bd490ab 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.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-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -2185,8 +2185,8 @@ let main files =
           "Oops, problem while fetching coq status."
         | Interface.Good status ->
           let path = match status.Interface.status_path with
-          | None -> ""
-          | Some p -> " in " ^ p
+          | [] | _ :: [] -> "" (* Drop the topmost level, usually "Top" *)
+          | _ :: l -> " in " ^ String.concat "." l
           in
           let name = match status.Interface.status_proofname with
           | None -> ""
@@ -2449,13 +2449,13 @@ let main files =
 	  try configure ~apply:update_notebook_pos ()
 	  with _ -> flash_info "Cannot save preferences"
 	end;
-	reset_revert_timer ()) ~stock:`PREFERENCES;
+	reset_revert_timer ()) ~accel:"<Ctrl>," ~stock:`PREFERENCES;
       (* GAction.add_action "Save preferences" ~label:"_Save preferences" ~callback:(fun _ -> save_pref ()); *) ];
     GAction.add_actions view_actions [
       GAction.add_action "View" ~label:"_View";
-      GAction.add_action "Previous tab" ~label:"_Previous tab" ~accel:("<SHIFT>Left") ~stock:`GO_BACK
+      GAction.add_action "Previous tab" ~label:"_Previous tab" ~accel:("<ALT>Left") ~stock:`GO_BACK
         ~callback:(fun _ -> session_notebook#previous_page ());
-      GAction.add_action "Next tab" ~label:"_Next tab" ~accel:("<SHIFT>Right") ~stock:`GO_FORWARD
+      GAction.add_action "Next tab" ~label:"_Next tab" ~accel:("<ALT>Right") ~stock:`GO_FORWARD
         ~callback:(fun _ -> session_notebook#next_page ());
       GAction.add_toggle_action "Show Toolbar" ~label:"Show _Toolbar"
         ~active:(!current.show_toolbar) ~callback:
@@ -2624,6 +2624,7 @@ let main files =
     Coqide_ui.ui_m#insert_action_group windows_actions 0;
     Coqide_ui.ui_m#insert_action_group help_actions 0;
     w#add_accel_group Coqide_ui.ui_m#get_accel_group ;
+    GtkMain.Rc.parse_string "gtk-can-change-accels = 1";
     if Coq_config.gtk_platform <> `QUARTZ
     then vbox#pack (Coqide_ui.ui_m#get_widget "/CoqIde MenuBar");
     let tbar = GtkButton.Toolbar.cast ((Coqide_ui.ui_m#get_widget "/CoqIde ToolBar")#as_widget)
diff --git a/ide/coqide.mli b/ide/coqide.mli
index 57158a6a..18df1f6a 100644
--- a/ide/coqide.mli
+++ b/ide/coqide.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-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/ide/coqide_main.ml4 b/ide/coqide_main.ml4
index 6f4b8b13..f5138311 100644
--- a/ide/coqide_main.ml4
+++ b/ide/coqide_main.ml4
@@ -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-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/ide/gtk_parsing.ml b/ide/gtk_parsing.ml
index c69f92e2..67f7e649 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-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/ide/ide_mac_stubs.c b/ide/ide_mac_stubs.c
index 64deb71d..2aeb2bf4 100644
--- a/ide/ide_mac_stubs.c
+++ b/ide/ide_mac_stubs.c
@@ -8,7 +8,7 @@
 #include <lablgtk2/wrappers.h>
 #include <lablgtk2/ml_glib.h>
 #include <lablgtk2/ml_gobject.h>
-#include <igemacintegration/gtkosxapplication.h>
+#include <gtkmacintegration/gtkosxapplication.h>
 
 GtkOSXApplication *theApp;
 value open_file_fun, forbid_quit_fun, themenubar, pref_item, about_item;
@@ -76,10 +76,10 @@ CAMLprim value caml_gtk_mac_ready(value menubar, value prefs, value about)
   caml_register_generational_global_root(&about_item);
   /*  gtk_accel_map_foreach(NULL, osx_accel_map_foreach_lcb);*/
   gtk_osxapplication_set_menu_bar(theApp,check_cast(GTK_MENU_SHELL,themenubar));
-  about_grp = gtk_osxapplication_add_app_menu_group(theApp);
-  pref_grp = gtk_osxapplication_add_app_menu_group(theApp);
-  gtk_osxapplication_add_app_menu_item(theApp,about_grp,check_cast(GTK_MENU_ITEM,about_item));
-  gtk_osxapplication_add_app_menu_item(theApp,pref_grp,check_cast(GTK_MENU_ITEM,pref_item));
+  gtk_osxapplication_insert_app_menu_item(theApp,check_cast(GTK_WIDGET,about_item),1);
+  gtk_osxapplication_insert_app_menu_item(theApp,gtk_separator_menu_item_new(),2);
+  gtk_osxapplication_insert_app_menu_item(theApp,check_cast(GTK_WIDGET,pref_item),3);
+  gtk_osxapplication_insert_app_menu_item(theApp,gtk_separator_menu_item_new(),4);
   gtk_osxapplication_ready(theApp);
   CAMLreturn(Val_unit);
 }
diff --git a/ide/ideproof.ml b/ide/ideproof.ml
index b79d6469..697e7f4f 100644
--- a/ide/ideproof.ml
+++ b/ide/ideproof.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-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -109,31 +109,39 @@ let mode_cesar (proof:GText.view) = function
       proof#buffer#insert ("thesis := \n "^cur_goal^"\n");
       ignore (proof#scroll_to_iter (proof#buffer#get_iter_at_mark `INSERT))
 
+let rec flatten = function
+| [] -> []
+| (lg, rg) :: l ->
+  let inner = flatten l in
+  List.rev_append lg inner @ rg
+
 let display mode (view:GText.view) goals hints evars =
   let () = view#buffer#set_text "" in
   match goals with
   | None -> ()
     (* No proof in progress *)
-  | Some { Interface.fg_goals = []; Interface.bg_goals = [] } ->
-    (* A proof has been finished, but not concluded *)
-    begin match evars with
-    | Some evs when evs <> [] ->
+  | Some { Interface.fg_goals = []; Interface.bg_goals = bg } ->
+    let bg = flatten (List.rev bg) in
+    let evars = match evars with None -> [] | Some evs -> evs in
+    begin match (bg, evars) with
+    | [], [] ->
+      view#buffer#insert "No more subgoals."
+    | [], _ :: _ ->
+      (* A proof has been finished, but not concluded *)
       view#buffer#insert "No more subgoals but non-instantiated existential variables:\n\n";
       let iter evar =
         let msg = Printf.sprintf "%s\n" evar.Interface.evar_info in
         view#buffer#insert msg
       in
-      List.iter iter evs
-    | _ ->
-      view#buffer#insert "No more subgoals."
+      List.iter iter evars
+    | _, _ ->
+      (* No foreground proofs, but still unfocused ones *)
+      view#buffer#insert "This subproof is complete, but there are still unfocused goals:\n\n";
+      let iter goal =
+        let msg = Printf.sprintf "%s\n" goal.Interface.goal_ccl in
+        view#buffer#insert msg
+      in
+      List.iter iter bg
     end
-  | Some { Interface.fg_goals = []; Interface.bg_goals = bg } ->
-    (* No foreground proofs, but still unfocused ones *)
-    view#buffer#insert "This subproof is complete, but there are still unfocused goals:\n\n";
-    let iter goal =
-      let msg = Printf.sprintf "%s\n" goal.Interface.goal_ccl in
-      view#buffer#insert msg
-    in
-    List.iter iter bg
   | Some { Interface.fg_goals = fg } ->
     mode view fg hints
diff --git a/ide/ideutils.ml b/ide/ideutils.ml
index a208ad0e..164c837a 100644
--- a/ide/ideutils.ml
+++ b/ide/ideutils.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-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/ide/ideutils.mli b/ide/ideutils.mli
index c433d92a..ff79d689 100644
--- a/ide/ideutils.mli
+++ b/ide/ideutils.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-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/ide/mac_default_accel_map b/ide/mac_default_accel_map
index 4d34636f..636447e3 100644
--- a/ide/mac_default_accel_map
+++ b/ide/mac_default_accel_map
@@ -1,372 +1,376 @@
-; coqide.opt GtkAccelMap rc-file         -*- scheme -*-
+; coqide GtkAccelMap rc-file         -*- scheme -*-
 ; this file is an automated accelerator map dump
 ;
-; (gtk_accel_path "<DEFAULT ROOT>/C_anonical Structure/" "")
-; (gtk_accel_path "<DEFAULT ROOT>/M_odule Type/" "")
-; (gtk_accel_path "<DEFAULT ROOT>/c_ompute/" "")
-; (gtk_accel_path "<CoqIde MenuBar>/Templates/_E.../" "")
-(gtk_accel_path "<Actions>/Templates/match" "<Shift><Meta>c")
-; (gtk_accel_path "<DEFAULT ROOT>/D_erive Inversion/" "")
-; (gtk_accel_path "<Actions>/Queries/Check" "F3")
-; (gtk_accel_path "<DEFAULT ROOT>/i_dtac/" "")
-; (gtk_accel_path "<DEFAULT ROOT>/L_oad/" "")
-; (gtk_accel_path "<DEFAULT ROOT>/a_ssert/" "")
-; (gtk_accel_path "<DEFAULT ROOT>/f_irstorder using/" "")
-; (gtk_accel_path "<DEFAULT ROOT>/s_olve/" "")
-; (gtk_accel_path "<CoqIde MenuBar>/Tactics/_l.../" "")
-(gtk_accel_path "<Actions>/Templates/Inductive" "<Shift><Meta>i")
-; (gtk_accel_path "<DEFAULT ROOT>/a_ssert (__:__)/" "")
-; (gtk_accel_path "<DEFAULT ROOT>/T_est Printing Synth/" "")
-; (gtk_accel_path "<CoqIde MenuBar>/Templates/_R.../" "")
-; (gtk_accel_path "<Actions>/Help/Browse Coq Library" "")
-; (gtk_accel_path "<DEFAULT ROOT>/U_nset Extraction Optimize/" "")
-; (gtk_accel_path "<DEFAULT ROOT>/s_imple inversion/" "")
-(gtk_accel_path "<Actions>/Edit/Copy" "<Meta>c")
-; (gtk_accel_path "<DEFAULT ROOT>/E_xtract Inductive/" "")
-(gtk_accel_path "<Actions>/Edit/Cut" "<Meta>x")
-; (gtk_accel_path "<DEFAULT ROOT>/i_nfo/" "")
-; (gtk_accel_path "<DEFAULT ROOT>/R_emove Printing If/" "")
-; (gtk_accel_path "<DEFAULT ROOT>/e_apply/" "")
-; (gtk_accel_path "<DEFAULT ROOT>/F_ixpoint/" "")
-; (gtk_accel_path "<DEFAULT ROOT>/c_hange __ in/" "")
-; (gtk_accel_path "<DEFAULT ROOT>/l_apply/" "")
-; (gtk_accel_path "<DEFAULT ROOT>/s_imple induction/" "")
-; (gtk_accel_path "<DEFAULT ROOT>/f_ail/" "")
-; (gtk_accel_path "<DEFAULT ROOT>/e_lim/" "")
-; (gtk_accel_path "<DEFAULT ROOT>/r_ewrite <- __ in/" "")
-; (gtk_accel_path "<DEFAULT ROOT>/A_dd Printing Let/" "")
-; (gtk_accel_path "<DEFAULT ROOT>/T_ransparent/" "")
-; (gtk_accel_path "<CoqIde MenuBar>/Tactics/_d.../" "")
-(gtk_accel_path "<Actions>/Tactics/Wizard" "<Meta><Control>dollar")
+; (gtk_accel_path "<Actions>/Templates/Template Read Module" "")
+; (gtk_accel_path "<Actions>/Tactics/Tactic pattern" "")
+(gtk_accel_path "<Actions>/Templates/Definition" "<Shift><Primary>d")
+; (gtk_accel_path "<Actions>/Templates/Template Program Lemma" "")
+(gtk_accel_path "<Actions>/Templates/Lemma" "<Shift><Primary>l")
+; (gtk_accel_path "<Actions>/Templates/Template Fact" "")
+(gtk_accel_path "<Actions>/Tactics/auto" "<Primary><Control>a")
+; (gtk_accel_path "<Actions>/Tactics/Tactic fold" "")
+; (gtk_accel_path "<Actions>/Help/About Coq" "")
+; (gtk_accel_path "<Actions>/Templates/Template Add Ring A Aplus Amult Aone Azero Ainv Aeq T [ c1 ... cn ]. " "")
+; (gtk_accel_path "<Actions>/Templates/Template Hypothesis" "")
+; (gtk_accel_path "<Actions>/Tactics/Tactic repeat" "")
+; (gtk_accel_path "<Actions>/Templates/Template Unset Extraction Optimize" "")
+; (gtk_accel_path "<Actions>/Templates/Template Add Printing Constructor" "")
 ; (gtk_accel_path "<Actions>/Windows/Detach View" "")
-; (gtk_accel_path "<DEFAULT ROOT>/T_heorem/" "")
-(gtk_accel_path "<Actions>/Templates/Scheme" "<Shift><Meta>s")
-; (gtk_accel_path "<DEFAULT ROOT>/R_emark/" "")
-; (gtk_accel_path "<Actions>/Compile/Compile" "")
-; (gtk_accel_path "<DEFAULT ROOT>/A_dd Relation/" "")
-; (gtk_accel_path "<DEFAULT ROOT>/r_ename __ into/" "")
-; (gtk_accel_path "<Actions>/File/Save as" "")
-; (gtk_accel_path "<DEFAULT ROOT>/f_irstorder/" "")
-; (gtk_accel_path "<DEFAULT ROOT>/G_rammar/" "")
-; (gtk_accel_path "<DEFAULT ROOT>/f_irstorder with/" "")
-; (gtk_accel_path "<DEFAULT ROOT>/r_ed/" "")
-; (gtk_accel_path "<DEFAULT ROOT>/D_efinition/" "")
-; (gtk_accel_path "<DEFAULT ROOT>/R_equire Import/" "")
-; (gtk_accel_path "<DEFAULT ROOT>/d_iscriminate/" "")
-; (gtk_accel_path "<DEFAULT ROOT>/i_ntro after/" "")
-; (gtk_accel_path "<Actions>/Export/Latex" "")
-; (gtk_accel_path "<DEFAULT ROOT>/j_p/" "")
-; (gtk_accel_path "<DEFAULT ROOT>/a_uto with/" "")
-; (gtk_accel_path "<DEFAULT ROOT>/S_ection/" "")
-; (gtk_accel_path "<DEFAULT ROOT>/r_ewrite/" "")
-; (gtk_accel_path "<Actions>/Export/Html" "")
-; (gtk_accel_path "<CoqIde MenuBar>/Tactics/_i.../" "")
-; (gtk_accel_path "<DEFAULT ROOT>/a_utorewrite/" "")
-; (gtk_accel_path "<DEFAULT ROOT>/F_ocus/" "")
-; (gtk_accel_path "<CoqIde MenuBar>/Templates/_O.../" "")
-; (gtk_accel_path "<DEFAULT ROOT>/l_azy in/" "")
-; (gtk_accel_path "<DEFAULT ROOT>/d_ependent inversion__clear __ with/" "")
-; (gtk_accel_path "<DEFAULT ROOT>/c_utrewrite/" "")
-(gtk_accel_path "<Actions>/Edit/Undo" "<Meta>u")
-; (gtk_accel_path "<DEFAULT ROOT>/c_onstructor __ with/" "")
-; (gtk_accel_path "<DEFAULT ROOT>/r_ing/" "")
-; (gtk_accel_path "<DEFAULT ROOT>/d_ependent rewrite <-/" "")
-; (gtk_accel_path "<DEFAULT ROOT>/e_limtype/" "")
-(gtk_accel_path "<Actions>/Tactics/simpl" "<Meta><Control>s")
-; (gtk_accel_path "<DEFAULT ROOT>/H_int/" "")
-; (gtk_accel_path "<DEFAULT ROOT>/H_int Rewrite/" "")
-; (gtk_accel_path "<DEFAULT ROOT>/V_ariable/" "")
-; (gtk_accel_path "<DEFAULT ROOT>/U_nset Implicit Arguments/" "")
-; (gtk_accel_path "<DEFAULT ROOT>/s_implify__eq/" "")
-; (gtk_accel_path "<Actions>/Compile/Next error" "F7")
-; (gtk_accel_path "<Actions>/Edit/Edit" "")
-; (gtk_accel_path "<DEFAULT ROOT>/S_et Extraction Optimize/" "")
-; (gtk_accel_path "<DEFAULT ROOT>/H_ypothesis/" "")
-; (gtk_accel_path "<DEFAULT ROOT>/E_nd Silent./" "")
-; (gtk_accel_path "<DEFAULT ROOT>/S_yntax/" "")
-; (gtk_accel_path "<DEFAULT ROOT>/d_ecide equality/" "")
-; (gtk_accel_path "<DEFAULT ROOT>/O_paque/" "")
-; (gtk_accel_path "<CoqIde MenuBar>/Templates/_T.../" "")
-; (gtk_accel_path "<CoqIde MenuBar>/Tactics/_a.../" "")
-; (gtk_accel_path "<CoqIde MenuBar>/Templates/_G.../" "")
-; (gtk_accel_path "<DEFAULT ROOT>/c_ase/" "")
-(gtk_accel_path "<Actions>/Navigation/Backward" "<Meta><Control>Up")
-; (gtk_accel_path "<DEFAULT ROOT>/C_oFixpoint/" "")
-; (gtk_accel_path "<DEFAULT ROOT>/P_rogram Fixpoint/" "")
-; (gtk_accel_path "<DEFAULT ROOT>/d_ependent inversion__clear/" "")
-; (gtk_accel_path "<DEFAULT ROOT>/c_ase __ with/" "")
-; (gtk_accel_path "<DEFAULT ROOT>/a_ssumption/" "")
-; (gtk_accel_path "<DEFAULT ROOT>/t_ransitivity/" "")
-; (gtk_accel_path "<DEFAULT ROOT>/i_ntros until/" "")
-; (gtk_accel_path "<DEFAULT ROOT>/s_plit/" "")
-; (gtk_accel_path "<DEFAULT ROOT>/e_xists/" "")
-(gtk_accel_path "<Actions>/Templates/Theorem" "<Shift><Meta>t")
-; (gtk_accel_path "<Actions>/Navigation/Navigation" "")
-; (gtk_accel_path "<DEFAULT ROOT>/H_int Unfold/" "")
-; (gtk_accel_path "<DEFAULT ROOT>/I_mplicit Arguments/" "")
-; (gtk_accel_path "<Actions>/Help/Help" "")
-; (gtk_accel_path "<DEFAULT ROOT>/d_ecompose sum/" "")
-; (gtk_accel_path "<DEFAULT ROOT>/A_dd Abstract Ring A Aplus Amult Aone Azero Ainv Aeq T./" "")
-; (gtk_accel_path "<CoqIde MenuBar>/Te_mplates/" "")
-(gtk_accel_path "<Actions>/Edit/Find in buffer" "<Meta>f")
-; (gtk_accel_path "<DEFAULT ROOT>/r_eplace __ with/" "")
-(gtk_accel_path "<Actions>/Tactics/omega" "<Meta><Control>o")
-; (gtk_accel_path "<DEFAULT ROOT>/S_cheme/" "")
-; (gtk_accel_path "<DEFAULT ROOT>/L_emma/" "")
-; (gtk_accel_path "<DEFAULT ROOT>/i_nversion__clear __ in/" "")
-; (gtk_accel_path "<DEFAULT ROOT>/E_xtraction Inline/" "")
-; (gtk_accel_path "<DEFAULT ROOT>/S_yntactic Definition/" "")
-; (gtk_accel_path "<DEFAULT ROOT>/i_nstantiate (__:=__)/" "")
-; (gtk_accel_path "<DEFAULT ROOT>/C_hapter/" "")
-; (gtk_accel_path "<CoqIde MenuBar>/Templates/_L.../" "")
-; (gtk_accel_path "<CoqIde MenuBar>/Tactics/_f.../" "")
-; (gtk_accel_path "<Actions>/Queries/Queries" "")
-; (gtk_accel_path "<DEFAULT ROOT>/T_est Printing Wildcard/" "")
-(gtk_accel_path "<Actions>/File/Open" "<Meta>o")
-; (gtk_accel_path "<DEFAULT ROOT>/f_old __ in/" "")
-(gtk_accel_path "<Actions>/Navigation/Go to" "<Meta><Control>Right")
+; (gtk_accel_path "<Actions>/Tactics/Tactic inversion" "")
+; (gtk_accel_path "<Actions>/Templates/Template Write State" "")
 ; (gtk_accel_path "<Actions>/Export/Export to" "")
-; (gtk_accel_path "<DEFAULT ROOT>/c_ongruence/" "")
-; (gtk_accel_path "<DEFAULT ROOT>/c_learbody/" "")
-(gtk_accel_path "<Actions>/File/Close buffer" "<Meta>w")
-; (gtk_accel_path "<DEFAULT ROOT>/a_pply/" "")
-; (gtk_accel_path "<Actions>/Queries/SearchAbout" "F2")
-; (gtk_accel_path "<DEFAULT ROOT>/i_ntro/" "")
-; (gtk_accel_path "<DEFAULT ROOT>/H_int Immediate/" "")
-; (gtk_accel_path "<DEFAULT ROOT>/p_ose __:=__)/" "")
-; (gtk_accel_path "<DEFAULT ROOT>/U_nset Undo/" "")
-; (gtk_accel_path "<CoqIde MenuBar>/Tactics/_s.../" "")
-; (gtk_accel_path "<DEFAULT ROOT>/P_rogram Definition/" "")
-; (gtk_accel_path "<DEFAULT ROOT>/R_equire/" "")
-; (gtk_accel_path "<DEFAULT ROOT>/c_ompare/" "")
-; (gtk_accel_path "<DEFAULT ROOT>/s_ymmetry in/" "")
-(gtk_accel_path "<Actions>/Display/Display coercions" "<Shift><Control>c")
-(gtk_accel_path "<Actions>/Navigation/Previous" "<Meta><Control>less")
-(gtk_accel_path "<Actions>/Display/Display all low-level contents" "<Shift><Control>l")
-; (gtk_accel_path "<DEFAULT ROOT>/C_oercion Local/" "")
-; (gtk_accel_path "<DEFAULT ROOT>/f_ix __ with/" "")
-; (gtk_accel_path "<DEFAULT ROOT>/A_dd ML Path/" "")
-; (gtk_accel_path "<DEFAULT ROOT>/A_xiom/" "")
-; (gtk_accel_path "<Actions>/Templates/Templates" "")
-; (gtk_accel_path "<DEFAULT ROOT>/a_bstract/" "")
-; (gtk_accel_path "<Actions>/Edit/Clear Undo Stack" "")
-(gtk_accel_path "<Actions>/File/New" "<Meta>n")
-; (gtk_accel_path "<CoqIde MenuBar>/Tactics/_hnf/" "")
-; (gtk_accel_path "<DEFAULT ROOT>/d_o/" "")
-; (gtk_accel_path "<DEFAULT ROOT>/E_xtract Constant/" "")
-; (gtk_accel_path "<DEFAULT ROOT>/E_nd/" "")
-; (gtk_accel_path "<CoqIde MenuBar>/Templates/_Qed./" "")
-; (gtk_accel_path "<DEFAULT ROOT>/A_dd Rec ML Path/" "")
-; (gtk_accel_path "<CoqIde MenuBar>/Templates/_D.../" "")
-(gtk_accel_path "<Actions>/Navigation/Hide" "<Meta><Control>h")
-; (gtk_accel_path "<DEFAULT ROOT>/c_ofix/" "")
-; (gtk_accel_path "<CoqIde MenuBar>/_Try Tactics/" "")
-; (gtk_accel_path "<DEFAULT ROOT>/S_et Printing Wildcard/" "")
-; (gtk_accel_path "<DEFAULT ROOT>/i_nversion__clear/" "")
-; (gtk_accel_path "<CoqIde MenuBar>/Templates/_V.../" "")
+(gtk_accel_path "<Actions>/Tactics/auto with *" "<Primary><Control>asterisk")
+; (gtk_accel_path "<Actions>/Tactics/Tactic inversion--clear" "")
+; (gtk_accel_path "<Actions>/Templates/Template Implicit Arguments" "")
+(gtk_accel_path "<Actions>/Edit/Find backwards" "<Primary>b")
+; (gtk_accel_path "<Actions>/Edit/Copy" "<Primary>c")
+; (gtk_accel_path "<Actions>/Tactics/Tactic inversion -- using" "")
+(gtk_accel_path "<Actions>/View/Previous tab" "<Control>Left")
+; (gtk_accel_path "<Actions>/Tactics/Tactic change -- in" "")
+; (gtk_accel_path "<Actions>/Tactics/Tactic jp" "")
+; (gtk_accel_path "<Actions>/Tactics/Tactic red" "")
+; (gtk_accel_path "<Actions>/Templates/Template Coercion" "")
+; (gtk_accel_path "<Actions>/Templates/Template CoFixpoint" "")
+; (gtk_accel_path "<Actions>/Tactics/Tactic intros until" "")
+; (gtk_accel_path "<Actions>/Templates/Template Derive Dependent Inversion" "")
+; (gtk_accel_path "<Actions>/Tactics/Tactic eapply" "")
+; (gtk_accel_path "<Actions>/View/View" "")
+; (gtk_accel_path "<Actions>/Tactics/Tactic change" "")
+; (gtk_accel_path "<Actions>/Tactics/Tactic firstorder using" "")
+; (gtk_accel_path "<Actions>/Tactics/Tactic decompose sum" "")
+; (gtk_accel_path "<Actions>/Tactics/Tactic cut" "")
+; (gtk_accel_path "<Actions>/Templates/Template Remove Printing Let" "")
+; (gtk_accel_path "<Actions>/Templates/Template Structure" "")
+; (gtk_accel_path "<Actions>/Tactics/Tactic compute in" "")
+; (gtk_accel_path "<Actions>/Queries/Locate" "")
+; (gtk_accel_path "<Actions>/Templates/Template Save." "")
+; (gtk_accel_path "<Actions>/Templates/Template Canonical Structure" "")
+; (gtk_accel_path "<Actions>/Tactics/Tactic compare" "")
+; (gtk_accel_path "<Actions>/Templates/Template Next Obligation" "")
+(gtk_accel_path "<Actions>/View/Display notations" "<Shift><Control>n")
+; (gtk_accel_path "<Actions>/Tactics/Tactic fail" "")
+; (gtk_accel_path "<Actions>/Tactics/Tactic left" "")
+(gtk_accel_path "<Actions>/Edit/Undo" "<Primary>u")
+(gtk_accel_path "<Actions>/Tactics/eauto with *" "<Primary><Control>ampersand")
+; (gtk_accel_path "<Actions>/Templates/Template Infix" "")
+; (gtk_accel_path "<Actions>/Tactics/Tactic functional induction" "")
+; (gtk_accel_path "<Actions>/Tactics/Tactic clear" "")
+; (gtk_accel_path "<Actions>/Templates/Template End Silent." "")
+; (gtk_accel_path "<Actions>/Tactics/Tactic intros" "")
+; (gtk_accel_path "<Actions>/Tactics/Tactic constructor -- with" "")
+; (gtk_accel_path "<Actions>/Tactics/Tactic destruct" "")
+; (gtk_accel_path "<Actions>/Tactics/Tactic intro after" "")
+; (gtk_accel_path "<Actions>/Tactics/Tactic abstract" "")
+; (gtk_accel_path "<Actions>/Queries/About" "F5")
+; (gtk_accel_path "<Actions>/Templates/Template CoInductive" "")
+; (gtk_accel_path "<Actions>/Templates/Template Unset Hyps--limit" "")
 ; (gtk_accel_path "<Actions>/Export/Ps" "")
-; (gtk_accel_path "<DEFAULT ROOT>/U_nset Hyps__limit/" "")
-; (gtk_accel_path "<DEFAULT ROOT>/H_int Extern/" "")
-; (gtk_accel_path "<DEFAULT ROOT>/f_unctional induction/" "")
-; (gtk_accel_path "<DEFAULT ROOT>/U_nset Extraction AutoInline/" "")
-; (gtk_accel_path "<DEFAULT ROOT>/U_nfocus/" "")
-; (gtk_accel_path "<Actions>/Edit/External editor" "")
-; (gtk_accel_path "<DEFAULT ROOT>/I_dentity Coercion/" "")
-; (gtk_accel_path "<DEFAULT ROOT>/a_bsurd/" "")
-; (gtk_accel_path "<DEFAULT ROOT>/c_hange/" "")
-(gtk_accel_path "<Actions>/Tactics/eauto" "<Meta><Control>e")
-; (gtk_accel_path "<DEFAULT ROOT>/O_bligations Tactic/" "")
-(gtk_accel_path "<Actions>/Tactics/trivial" "<Meta><Control>v")
-; (gtk_accel_path "<DEFAULT ROOT>/d_ependent inversion/" "")
-; (gtk_accel_path "<DEFAULT ROOT>/c_bv/" "")
-; (gtk_accel_path "<DEFAULT ROOT>/A_dd Ring A Aplus Amult Aone Azero Ainv Aeq T [ c1 ... cn ]. /" "")
-; (gtk_accel_path "<DEFAULT ROOT>/p_ose/" "")
-; (gtk_accel_path "<DEFAULT ROOT>/s_et (__:=__)/" "")
-; (gtk_accel_path "<DEFAULT ROOT>/R_equire Export/" "")
-; (gtk_accel_path "<DEFAULT ROOT>/L_tac/" "")
-; (gtk_accel_path "<DEFAULT ROOT>/A_dd Rec LoadPath/" "")
-; (gtk_accel_path "<CoqIde MenuBar>/Tactics/_c.../" "")
-(gtk_accel_path "<Actions>/Navigation/End" "<Meta><Control>End")
-(gtk_accel_path "<Actions>/Templates/Lemma" "<Shift><Meta>l")
-(gtk_accel_path "<Actions>/Navigation/Start" "<Meta><Control>Home")
-; (gtk_accel_path "<CoqIde MenuBar>/Templates/_I.../" "")
-(gtk_accel_path "<Actions>/File/Print..." "<Meta>p")
-; (gtk_accel_path "<DEFAULT ROOT>/d_ependent rewrite ->/" "")
-; (gtk_accel_path "<DEFAULT ROOT>/S_tructure/" "")
-; (gtk_accel_path "<DEFAULT ROOT>/T_est Printing Let/" "")
-; (gtk_accel_path "<DEFAULT ROOT>/T_ime/" "")
-; (gtk_accel_path "<DEFAULT ROOT>/g_eneralize/" "")
-(gtk_accel_path "<Actions>/Display/Display all basic low-level contents" "<Shift><Control>a")
-; (gtk_accel_path "<CoqIde MenuBar>/Tactics/_p.../" "")
-; (gtk_accel_path "<DEFAULT ROOT>/f_old/" "")
-; (gtk_accel_path "<DEFAULT ROOT>/H_int Resolve/" "")
-; (gtk_accel_path "<DEFAULT ROOT>/M_utual Inductive/" "")
-; (gtk_accel_path "<DEFAULT ROOT>/i_nversion __ in/" "")
-; (gtk_accel_path "<Actions>/Windows/Show/Hide Toolbar" "")
-(gtk_accel_path "<Actions>/File/Save" "<Meta>s")
-; (gtk_accel_path "<Actions>/File/Save all" "")
-; (gtk_accel_path "<Actions>/Queries/Print" "F4")
-; (gtk_accel_path "<DEFAULT ROOT>/c_onstructor/" "")
-; (gtk_accel_path "<Actions>/Export/Dvi" "")
-; (gtk_accel_path "<DEFAULT ROOT>/s_etoid__replace/" "")
-; (gtk_accel_path "<DEFAULT ROOT>/D_efined./" "")
-; (gtk_accel_path "<DEFAULT ROOT>/I_nfix/" "")
-(gtk_accel_path "<Actions>/Navigation/Next" "<Meta><Control>greater")
-; (gtk_accel_path "<DEFAULT ROOT>/A_dd Morphism/" "")
+; (gtk_accel_path "<Actions>/Tactics/Tactic elim" "")
+; (gtk_accel_path "<Actions>/Templates/Template Transparent" "")
+; (gtk_accel_path "<Actions>/Tactics/Tactic assert (--:--)" "")
+; (gtk_accel_path "<Actions>/Templates/Template Add Rec LoadPath" "")
+; (gtk_accel_path "<Actions>/Templates/Template Extract Constant" "")
+; (gtk_accel_path "<Actions>/Tactics/Tactic compute" "")
+; (gtk_accel_path "<Actions>/Compile/Next error" "F7")
+; (gtk_accel_path "<Actions>/Templates/Template Add ML Path" "")
+; (gtk_accel_path "<Actions>/Templates/Template Test Printing Wildcard" "")
+; (gtk_accel_path "<Actions>/Templates/Template Set Implicit Arguments" "")
+; (gtk_accel_path "<Actions>/Templates/Template Test Printing Let" "")
 ; (gtk_accel_path "<Actions>/Windows/Windows" "")
-; (gtk_accel_path "<DEFAULT ROOT>/e_xact/" "")
-; (gtk_accel_path "<DEFAULT ROOT>/c_bv in/" "")
-; (gtk_accel_path "<DEFAULT ROOT>/t_ry/" "")
-; (gtk_accel_path "<CoqIde MenuBar>/Templates/_A.../" "")
-(gtk_accel_path "<Actions>/Display/Display notations" "<Shift><Control>n")
-; (gtk_accel_path "<DEFAULT ROOT>/c_lear/" "")
+; (gtk_accel_path "<Actions>/Templates/Template Defined." "")
+(gtk_accel_path "<Actions>/Templates/match" "<Shift><Primary>c")
+; (gtk_accel_path "<Actions>/Tactics/Tactic set (--:=--)" "")
+; (gtk_accel_path "<Actions>/Templates/Template Test Printing If" "")
 ; (gtk_accel_path "<Actions>/Compile/Make" "F6")
-(gtk_accel_path "<Actions>/Tactics/eauto with *" "<Meta><Control>ampersand")
-; (gtk_accel_path "<Actions>/Help/Browse Coq Manual" "")
-; (gtk_accel_path "<CoqIde MenuBar>/Templates/_N.../" "")
-(gtk_accel_path "<Actions>/File/Quit" "<Meta>q")
-; (gtk_accel_path "<DEFAULT ROOT>/u_nfold/" "")
-; (gtk_accel_path "<CoqIde MenuBar>/Tactics/_u.../" "")
-; (gtk_accel_path "<DEFAULT ROOT>/d_ouble induction/" "")
-; (gtk_accel_path "<DEFAULT ROOT>/S_et Silent./" "")
-; (gtk_accel_path "<DEFAULT ROOT>/V_ariables/" "")
-; (gtk_accel_path "<DEFAULT ROOT>/U_nset Printing Wildcard/" "")
-; (gtk_accel_path "<DEFAULT ROOT>/r_ewrite <-/" "")
-; (gtk_accel_path "<DEFAULT ROOT>/I_nductive/" "")
-; (gtk_accel_path "<DEFAULT ROOT>/e_auto with/" "")
-; (gtk_accel_path "<DEFAULT ROOT>/r_epeat/" "")
-; (gtk_accel_path "<Actions>/Queries/Locate" "")
-; (gtk_accel_path "<DEFAULT ROOT>/S_et Hyps__limit/" "")
-; (gtk_accel_path "<DEFAULT ROOT>/A_dd Abstract Semi Ring A Aplus Amult Aone Azero Aeq T./" "")
-; (gtk_accel_path "<DEFAULT ROOT>/c_ompute in/" "")
-; (gtk_accel_path "<CoqIde MenuBar>/Templates/_F.../" "")
-; (gtk_accel_path "<DEFAULT ROOT>/G_lobal Variable/" "")
-; (gtk_accel_path "<DEFAULT ROOT>/t_auto/" "")
-; (gtk_accel_path "<DEFAULT ROOT>/E_xtraction NoInline/" "")
-; (gtk_accel_path "<DEFAULT ROOT>/u_nfold __ in/" "")
-; (gtk_accel_path "<DEFAULT ROOT>/s_imple destruct/" "")
-(gtk_accel_path "<Actions>/Navigation/Interrupt" "<Meta><Control>Break")
-; (gtk_accel_path "<CoqIde MenuBar>/Templates/_S.../" "")
-; (gtk_accel_path "<DEFAULT ROOT>/i_njection/" "")
-; (gtk_accel_path "<DEFAULT ROOT>/R_ead Module/" "")
-; (gtk_accel_path "<DEFAULT ROOT>/P_rogram Lemma/" "")
-; (gtk_accel_path "<DEFAULT ROOT>/U_nset Silent./" "")
-(gtk_accel_path "<Actions>/Display/Display universe levels" "<Shift><Control>u")
-; (gtk_accel_path "<DEFAULT ROOT>/f_ourier/" "")
-; (gtk_accel_path "<DEFAULT ROOT>/D_erive Inversion__clear/" "")
-; (gtk_accel_path "<CoqIde MenuBar>/Tactics/_omega/" "")
-; (gtk_accel_path "<DEFAULT ROOT>/S_et Undo/" "")
-; (gtk_accel_path "<DEFAULT ROOT>/A_dd Semi Ring A Aplus Amult Aone Azero Aeq T [ c1 ... cn ]./" "")
-; (gtk_accel_path "<DEFAULT ROOT>/s_impl __ in/" "")
-; (gtk_accel_path "<Actions>/Windows/Show/Hide Query Pane" "Escape")
-; (gtk_accel_path "<DEFAULT ROOT>/R_estore State/" "")
-; (gtk_accel_path "<DEFAULT ROOT>/R_emove Printing Let/" "")
-; (gtk_accel_path "<DEFAULT ROOT>/A_dd Printing If/" "")
-(gtk_accel_path "<Actions>/Tactics/tauto" "<Meta><Control>p")
-; (gtk_accel_path "<DEFAULT ROOT>/s_impl/" "")
-; (gtk_accel_path "<DEFAULT ROOT>/i_ntros/" "")
-; (gtk_accel_path "<DEFAULT ROOT>/s_ymmetry/" "")
-; (gtk_accel_path "<DEFAULT ROOT>/c_ut/" "")
-; (gtk_accel_path "<DEFAULT ROOT>/r_efine/" "")
-; (gtk_accel_path "<CoqIde MenuBar>/Tactics/_e.../" "")
-; (gtk_accel_path "<DEFAULT ROOT>/e_exact/" "")
-(gtk_accel_path "<Actions>/Navigation/Forward" "<Meta><Control>Down")
-(gtk_accel_path "<Actions>/Edit/Paste" "<Meta>v")
-; (gtk_accel_path "<DEFAULT ROOT>/C_oercion/" "")
-; (gtk_accel_path "<CoqIde MenuBar>/Tactics/_r.../" "")
-; (gtk_accel_path "<DEFAULT ROOT>/d_estruct/" "")
-; (gtk_accel_path "<DEFAULT ROOT>/A_dd Setoid/" "")
-; (gtk_accel_path "<Actions>/Queries/Whelp Locate" "")
-; (gtk_accel_path "<DEFAULT ROOT>/T_est Printing If/" "")
-; (gtk_accel_path "<Actions>/Display/Display" "")
-; (gtk_accel_path "<CoqIde MenuBar>/Tactics/_move __ after/" "")
-(gtk_accel_path "<Actions>/Edit/Complete Word" "<Meta>slash")
-; (gtk_accel_path "<DEFAULT ROOT>/s_ubst/" "")
-; (gtk_accel_path "<Actions>/Help/About Coq" "")
-; (gtk_accel_path "<DEFAULT ROOT>/s_etoid__rewrite/" "")
+; (gtk_accel_path "<Actions>/Templates/Template Module Type" "")
+; (gtk_accel_path "<Actions>/Tactics/Tactic apply -- with" "")
+; (gtk_accel_path "<Actions>/File/Save as" "")
+; (gtk_accel_path "<Actions>/Templates/Template Remove Printing Constructor" "")
+; (gtk_accel_path "<Actions>/Templates/Template Set Hyps--limit" "")
+; (gtk_accel_path "<Actions>/Templates/Template Global Variable" "")
+; (gtk_accel_path "<Actions>/Tactics/Tactic trivial" "")
+; (gtk_accel_path "<Actions>/Templates/Template Add Setoid" "")
+; (gtk_accel_path "<Actions>/Templates/Template Proof." "")
+; (gtk_accel_path "<Actions>/Templates/Template Load Verbose" "")
+; (gtk_accel_path "<Actions>/Compile/Compile buffer" "")
+; (gtk_accel_path "<Actions>/Queries/Print" "F4")
+; (gtk_accel_path "<Actions>/Templates/Template Obligations Tactic" "")
+; (gtk_accel_path "<Actions>/Tactics/Tactic cbv" "")
+; (gtk_accel_path "<Actions>/Tactics/Tactic first" "")
+; (gtk_accel_path "<Actions>/Tactics/Tactic case" "")
+; (gtk_accel_path "<Actions>/Templates/Template Hint Constructors" "")
+; (gtk_accel_path "<Actions>/Templates/Template Add Abstract Ring A Aplus Amult Aone Azero Ainv Aeq T." "")
+; (gtk_accel_path "<Actions>/Templates/Template Coercion Local" "")
+; (gtk_accel_path "<Actions>/View/Show Query Pane" "Escape")
+; (gtk_accel_path "<Actions>/Templates/Template Add Relation" "")
+; (gtk_accel_path "<Actions>/Tactics/Tactic inversion--clear -- in" "")
+; (gtk_accel_path "<Actions>/Templates/Template Definition" "")
+; (gtk_accel_path "<Actions>/Templates/Template Add Rec ML Path" "")
+; (gtk_accel_path "<Actions>/Tactics/Tactic apply" "")
+; (gtk_accel_path "<Actions>/Export/Latex" "")
+; (gtk_accel_path "<Actions>/Tactics/Tactic inversion -- using -- in" "")
+; (gtk_accel_path "<Actions>/Tactics/Tactic generalize" "")
+; (gtk_accel_path "<Actions>/Templates/Template Reset Extraction Inline" "")
+(gtk_accel_path "<Actions>/Navigation/Hide" "<Primary><Control>h")
+; (gtk_accel_path "<Actions>/File/Close buffer" "<Primary>w")
+; (gtk_accel_path "<Actions>/Tactics/Tactic induction" "")
+; (gtk_accel_path "<Actions>/Tactics/Tactic eauto with" "")
+(gtk_accel_path "<Actions>/View/Display raw matching expressions" "<Shift><Control>m")
+(gtk_accel_path "<Actions>/Navigation/Backward" "<Primary><Control>Up")
+; (gtk_accel_path "<Actions>/Tactics/Tactic u" "")
+; (gtk_accel_path "<Actions>/Templates/Templates" "")
+; (gtk_accel_path "<Actions>/Tactics/Tactic p" "")
+; (gtk_accel_path "<Actions>/Tactics/Tactic lapply" "")
+; (gtk_accel_path "<Actions>/Tactics/Tactic t" "")
+; (gtk_accel_path "<Actions>/Tactics/Tactic s" "")
+; (gtk_accel_path "<Actions>/Tactics/Tactic r" "")
+; (gtk_accel_path "<Actions>/Tactics/Tactic case -- with" "")
+; (gtk_accel_path "<Actions>/Tactics/Tactic eexact" "")
+; (gtk_accel_path "<Actions>/Queries/Check" "F3")
+; (gtk_accel_path "<Actions>/Tactics/Tactic omega" "")
+; (gtk_accel_path "<Actions>/File/New" "<Primary>n")
+; (gtk_accel_path "<Actions>/Tactics/Tactic l" "")
+; (gtk_accel_path "<Actions>/Tactics/Tactic intro" "")
+; (gtk_accel_path "<Actions>/Tactics/Tactic j" "")
+; (gtk_accel_path "<Actions>/Tactics/Tactic i" "")
+; (gtk_accel_path "<Actions>/Tactics/Tactic e" "")
+; (gtk_accel_path "<Actions>/Tactics/Tactic g" "")
+; (gtk_accel_path "<Actions>/Tactics/Tactic f" "")
+; (gtk_accel_path "<Actions>/Tactics/Tactic d" "")
+; (gtk_accel_path "<Actions>/Tactics/Tactic c" "")
+(gtk_accel_path "<Actions>/File/Rehighlight" "<Primary>l")
+; (gtk_accel_path "<Actions>/Tactics/Tactic simple inversion" "")
+; (gtk_accel_path "<Actions>/Tactics/Tactic a" "")
+; (gtk_accel_path "<Actions>/Templates/Template Mutual Inductive" "")
+; (gtk_accel_path "<Actions>/Templates/Template Extraction NoInline" "")
+(gtk_accel_path "<Actions>/Templates/Theorem" "<Shift><Primary>t")
+; (gtk_accel_path "<Actions>/Templates/Template Derive Dependent Inversion--clear" "")
+; (gtk_accel_path "<Actions>/Tactics/Tactic unfold" "")
 ; (gtk_accel_path "<Actions>/Tactics/Try Tactics" "")
-; (gtk_accel_path "<CoqIde MenuBar>/Templates/_C.../" "")
-; (gtk_accel_path "<DEFAULT ROOT>/L_ocal/" "")
-; (gtk_accel_path "<DEFAULT ROOT>/s_et/" "")
-; (gtk_accel_path "<CoqIde MenuBar>/Tactics/_quote/" "")
-(gtk_accel_path "<Actions>/Templates/Definition" "<Shift><Meta>d")
-; (gtk_accel_path "<DEFAULT ROOT>/S_et Implicit Arguments/" "")
+; (gtk_accel_path "<Actions>/Tactics/Tactic red in" "")
+; (gtk_accel_path "<Actions>/Tactics/Tactic rewrite <- -- in" "")
+; (gtk_accel_path "<Actions>/Templates/Template Hint Extern" "")
+; (gtk_accel_path "<Actions>/Templates/Template Unfocus" "")
+; (gtk_accel_path "<Actions>/Tactics/Tactic dependent inversion--clear" "")
+; (gtk_accel_path "<Actions>/Help/Browse Coq Library" "")
+; (gtk_accel_path "<Actions>/Tactics/Tactic lazy" "")
+; (gtk_accel_path "<Actions>/Templates/Template Scheme" "")
+(gtk_accel_path "<Actions>/Tactics/tauto" "<Primary><Control>p")
+; (gtk_accel_path "<Actions>/Tactics/Tactic cutrewrite" "")
+; (gtk_accel_path "<Actions>/Tactics/Tactic contradiction" "")
+; (gtk_accel_path "<Actions>/Templates/Template Set Printing Wildcard" "")
+; (gtk_accel_path "<Actions>/Templates/Template Add LoadPath" "")
+(gtk_accel_path "<Actions>/Navigation/Previous" "<Primary><Control>less")
+; (gtk_accel_path "<Actions>/Templates/Template Require" "")
+; (gtk_accel_path "<Actions>/Tactics/Tactic simpl" "")
+; (gtk_accel_path "<Actions>/Templates/Template Require Import" "")
+; (gtk_accel_path "<Actions>/Templates/Template Add Abstract Semi Ring A Aplus Amult Aone Azero Aeq T." "")
+(gtk_accel_path "<Actions>/Navigation/Forward" "<Primary><Control>Down")
+; (gtk_accel_path "<Actions>/Tactics/Tactic rename -- into" "")
+; (gtk_accel_path "<Actions>/Compile/Compile" "")
+; (gtk_accel_path "<Actions>/File/Save all" "")
+; (gtk_accel_path "<Actions>/Tactics/Tactic fix" "")
+; (gtk_accel_path "<Actions>/Templates/Template Parameter" "")
+; (gtk_accel_path "<Actions>/Tactics/Tactic assert" "")
+; (gtk_accel_path "<Actions>/Tactics/Tactic do" "")
+; (gtk_accel_path "<Actions>/Tactics/Tactic ring" "")
+; (gtk_accel_path "<Actions>/Export/Pdf" "")
+; (gtk_accel_path "<Actions>/Tactics/Tactic quote" "")
+; (gtk_accel_path "<Actions>/Tactics/Tactic symmetry in" "")
+; (gtk_accel_path "<Actions>/Help/Help" "")
+(gtk_accel_path "<Actions>/Templates/Inductive" "<Shift><Primary>i")
+; (gtk_accel_path "<Actions>/Edit/Clear Undo Stack" "")
+; (gtk_accel_path "<Actions>/Tactics/Tactic intro -- after" "")
+; (gtk_accel_path "<Actions>/Templates/Template Syntax" "")
+; (gtk_accel_path "<Actions>/Tactics/Tactic idtac" "")
+; (gtk_accel_path "<Actions>/Tactics/Tactic fold -- in" "")
+; (gtk_accel_path "<Actions>/Templates/Template Program Definition" "")
+(gtk_accel_path "<Actions>/Tactics/Wizard" "<Primary><Control>dollar")
+; (gtk_accel_path "<Actions>/Templates/Template Hint Resolve" "")
+; (gtk_accel_path "<Actions>/Templates/Template Set Extraction Optimize" "")
 ; (gtk_accel_path "<Actions>/File/Revert all buffers" "")
-; (gtk_accel_path "<CoqIde MenuBar>/Templates/_P.../" "")
-; (gtk_accel_path "<DEFAULT ROOT>/t_rivial/" "")
-(gtk_accel_path "<Actions>/Display/Display existential variable instances" "<Shift><Control>e")
-; (gtk_accel_path "<CoqIde MenuBar>/Tactics/_j.../" "")
-; (gtk_accel_path "<DEFAULT ROOT>/A_dd LoadPath/" "")
-; (gtk_accel_path "<DEFAULT ROOT>/N_otation/" "")
-; (gtk_accel_path "<Actions>/Edit/Preferences" "")
-; (gtk_accel_path "<DEFAULT ROOT>/L_oad Verbose/" "")
-; (gtk_accel_path "<DEFAULT ROOT>/i_ntro __ after/" "")
-; (gtk_accel_path "<DEFAULT ROOT>/D_erive Dependent Inversion/" "")
-; (gtk_accel_path "<DEFAULT ROOT>/d_ependent inversion __ with/" "")
-; (gtk_accel_path "<DEFAULT ROOT>/P_rogram Theorem/" "")
-; (gtk_accel_path "<DEFAULT ROOT>/E_xtraction Language/" "")
-; (gtk_accel_path "<CoqIde MenuBar>/Templates/_U.../" "")
-(gtk_accel_path "<Actions>/Display/Display raw matching expressions" "<Shift><Control>m")
-; (gtk_accel_path "<DEFAULT ROOT>/c_asetype/" "")
-(gtk_accel_path "<Actions>/Edit/Find backwards" "<Meta>b")
-; (gtk_accel_path "<DEFAULT ROOT>/S_ave./" "")
-; (gtk_accel_path "<DEFAULT ROOT>/p_attern/" "")
-; (gtk_accel_path "<DEFAULT ROOT>/M_odule/" "")
-; (gtk_accel_path "<DEFAULT ROOT>/D_eclare ML Module/" "")
-; (gtk_accel_path "<CoqIde MenuBar>/Templates/_H.../" "")
-; (gtk_accel_path "<DEFAULT ROOT>/F_act/" "")
-; (gtk_accel_path "<DEFAULT ROOT>/A_dd Field/" "")
-; (gtk_accel_path "<DEFAULT ROOT>/R_emove LoadPath/" "")
-; (gtk_accel_path "<CoqIde MenuBar>/Templates/_Write State/" "")
+; (gtk_accel_path "<Actions>/Tactics/Tactic subst" "")
+; (gtk_accel_path "<Actions>/Tactics/Tactic autorewrite" "")
+; (gtk_accel_path "<Actions>/Tactics/Tactic pose" "")
+; (gtk_accel_path "<Actions>/Tactics/Tactic simplify--eq" "")
+; (gtk_accel_path "<Actions>/Tactics/Tactic clearbody" "")
+; (gtk_accel_path "<Actions>/Tactics/Tactic eauto" "")
+; (gtk_accel_path "<Actions>/Templates/Template Grammar" "")
+; (gtk_accel_path "<Actions>/Tactics/Tactic exact" "")
+; (gtk_accel_path "<Actions>/Templates/Template Unset Implicit Arguments" "")
+; (gtk_accel_path "<Actions>/Templates/Template Extract Inductive" "")
+(gtk_accel_path "<Actions>/View/Display implicit arguments" "<Shift><Control>i")
+; (gtk_accel_path "<Actions>/Tactics/Tactic symmetry" "")
+; (gtk_accel_path "<Actions>/Templates/Template Add Printing Let" "")
+; (gtk_accel_path "<Actions>/Help/Help for keyword" "<Primary>h")
+; (gtk_accel_path "<Actions>/File/Save" "<Primary>s")
 ; (gtk_accel_path "<Actions>/Compile/Make makefile" "")
-; (gtk_accel_path "<DEFAULT ROOT>/C_oInductive/" "")
-; (gtk_accel_path "<Actions>/Compile/Compile buffer" "")
-; (gtk_accel_path "<DEFAULT ROOT>/l_eft/" "")
-; (gtk_accel_path "<DEFAULT ROOT>/a_pply __ with/" "")
-(gtk_accel_path "<Actions>/File/Rehighlight" "<Meta>l")
+; (gtk_accel_path "<Actions>/Templates/Template Remove LoadPath" "")
+(gtk_accel_path "<Actions>/Navigation/Interrupt" "<Primary><Control>Break")
+(gtk_accel_path "<Actions>/Navigation/End" "<Primary><Control>End")
+; (gtk_accel_path "<Actions>/Templates/Template Add Morphism" "")
+; (gtk_accel_path "<Actions>/Tactics/Tactic field" "")
+; (gtk_accel_path "<Actions>/Templates/Template Axiom" "")
+; (gtk_accel_path "<Actions>/Tactics/Tactic solve" "")
+; (gtk_accel_path "<Actions>/Tactics/Tactic casetype" "")
+; (gtk_accel_path "<Actions>/Tactics/Tactic cbv in" "")
+; (gtk_accel_path "<Actions>/Templates/Template Load" "")
+; (gtk_accel_path "<Actions>/Tactics/Tactic fourier" "")
+; (gtk_accel_path "<Actions>/Templates/Template Goal" "")
+; (gtk_accel_path "<Actions>/Tactics/Tactic exists" "")
+; (gtk_accel_path "<Actions>/Tactics/Tactic decompose record" "")
+(gtk_accel_path "<Actions>/Navigation/Go to" "<Primary><Control>Right")
+; (gtk_accel_path "<Actions>/Templates/Template Remark" "")
+; (gtk_accel_path "<Actions>/Templates/Template Set Undo" "")
+; (gtk_accel_path "<Actions>/Templates/Template Inductive" "")
+(gtk_accel_path "<Actions>/Edit/Preferences" "<Primary>VoidSymbol")
+; (gtk_accel_path "<Actions>/Export/Html" "")
+; (gtk_accel_path "<Actions>/Templates/Template Extraction Inline" "")
+; (gtk_accel_path "<Actions>/Tactics/Tactic absurd" "")
+(gtk_accel_path "<Actions>/Tactics/intuition" "<Primary><Control>i")
+; (gtk_accel_path "<Actions>/Tactics/Tactic simple induction" "")
+; (gtk_accel_path "<Actions>/Queries/Queries" "")
+; (gtk_accel_path "<Actions>/Tactics/Tactic rewrite -- in" "")
+; (gtk_accel_path "<Actions>/Templates/Template Hint Rewrite" "")
+; (gtk_accel_path "<Actions>/Templates/Template Add Semi Ring A Aplus Amult Aone Azero Aeq T [ c1 ... cn ]." "")
+; (gtk_accel_path "<Actions>/Navigation/Navigation" "")
+; (gtk_accel_path "<Actions>/Help/Browse Coq Manual" "")
+; (gtk_accel_path "<Actions>/Tactics/Tactic transitivity" "")
+; (gtk_accel_path "<Actions>/Tactics/Tactic auto" "")
+; (gtk_accel_path "<Actions>/Tactics/Tactic dependent inversion -- with" "")
+; (gtk_accel_path "<Actions>/Tactics/Tactic assumption" "")
+; (gtk_accel_path "<Actions>/Templates/Template Notation" "")
+; (gtk_accel_path "<Actions>/Edit/Cut" "<Primary>x")
+; (gtk_accel_path "<Actions>/Templates/Template Theorem" "")
+; (gtk_accel_path "<Actions>/Templates/Template Unset Printing Wildcard" "")
+; (gtk_accel_path "<Actions>/Tactics/Tactic constructor" "")
+; (gtk_accel_path "<Actions>/Templates/Template Identity Coercion" "")
+; (gtk_accel_path "<Actions>/Queries/Whelp Locate" "")
+(gtk_accel_path "<Actions>/View/Display all low-level contents" "<Shift><Control>l")
+; (gtk_accel_path "<Actions>/Tactics/Tactic right" "")
+; (gtk_accel_path "<Actions>/Tactics/Tactic elim -- with" "")
+; (gtk_accel_path "<Actions>/Tactics/Tactic cofix" "")
+; (gtk_accel_path "<Actions>/Templates/Template Restore State" "")
+; (gtk_accel_path "<Actions>/Templates/Template Lemma" "")
+; (gtk_accel_path "<Actions>/Tactics/Tactic refine" "")
+; (gtk_accel_path "<Actions>/Templates/Template Section" "")
+; (gtk_accel_path "<Actions>/Tactics/Tactic assert (--:=--)" "")
+; (gtk_accel_path "<Actions>/Edit/Find in buffer" "<Primary>f")
+; (gtk_accel_path "<Actions>/Tactics/Tactic progress" "")
+; (gtk_accel_path "<Actions>/Templates/Template Add Printing If" "")
+; (gtk_accel_path "<Actions>/Templates/Template Chapter" "")
+(gtk_accel_path "<Actions>/File/Print..." "<Primary>p")
+; (gtk_accel_path "<Actions>/Templates/Template Record" "")
+; (gtk_accel_path "<Actions>/Tactics/Tactic info" "")
+; (gtk_accel_path "<Actions>/Tactics/Tactic firstorder with" "")
+; (gtk_accel_path "<Actions>/Templates/Template Hint Unfold" "")
+; (gtk_accel_path "<Actions>/Templates/Template Set Silent." "")
+; (gtk_accel_path "<Actions>/Templates/Template Program Theorem" "")
+; (gtk_accel_path "<Actions>/Templates/Template Declare ML Module" "")
+; (gtk_accel_path "<Actions>/Tactics/Tactic lazy in" "")
+; (gtk_accel_path "<Actions>/Tactics/Tactic unfold -- in" "")
+; (gtk_accel_path "<Actions>/Edit/Paste" "<Primary>v")
+; (gtk_accel_path "<Actions>/Templates/Template Remove Printing If" "")
+; (gtk_accel_path "<Actions>/Tactics/Tactic intuition" "")
+; (gtk_accel_path "<Actions>/Queries/SearchAbout" "F2")
+; (gtk_accel_path "<Actions>/Tactics/Tactic dependent rewrite ->" "")
+; (gtk_accel_path "<Actions>/Templates/Template Module" "")
+; (gtk_accel_path "<Actions>/Templates/Template Unset Extraction AutoInline" "")
+(gtk_accel_path "<Actions>/Templates/Scheme" "<Shift><Primary>s")
+; (gtk_accel_path "<Actions>/Templates/Template V" "")
+; (gtk_accel_path "<Actions>/Templates/Template Variable" "")
+; (gtk_accel_path "<Actions>/Tactics/Tactic decide equality" "")
+; (gtk_accel_path "<Actions>/Tactics/Tactic instantiate (--:=--)" "")
+; (gtk_accel_path "<Actions>/Templates/Template Syntactic Definition" "")
+; (gtk_accel_path "<Actions>/Templates/Template Set Extraction AutoInline" "")
+; (gtk_accel_path "<Actions>/Templates/Template Unset Undo" "")
+; (gtk_accel_path "<Actions>/Tactics/Tactic dependent inversion" "")
+; (gtk_accel_path "<Actions>/Templates/Template Add Field" "")
+; (gtk_accel_path "<Actions>/Tactics/Tactic setoid--rewrite" "")
+; (gtk_accel_path "<Actions>/Templates/Template Require Export" "")
+; (gtk_accel_path "<Actions>/Tactics/Tactic rewrite <-" "")
+(gtk_accel_path "<Actions>/Tactics/omega" "<Primary><Control>o")
+; (gtk_accel_path "<Actions>/Tactics/Tactic split" "")
+; (gtk_accel_path "<Actions>/File/Quit" "<Primary>q")
+(gtk_accel_path "<Actions>/View/Display existential variable instances" "<Shift><Control>e")
+(gtk_accel_path "<Actions>/Navigation/Start" "<Primary><Control>Home")
+; (gtk_accel_path "<Actions>/Tactics/Tactic dependent rewrite <-" "")
+; (gtk_accel_path "<Actions>/Templates/Template U" "")
+; (gtk_accel_path "<Actions>/Templates/Template Variables" "")
+; (gtk_accel_path "<Actions>/Templates/Template S" "")
+; (gtk_accel_path "<Actions>/Tactics/Tactic move -- after" "")
+; (gtk_accel_path "<Actions>/Templates/Template Unset Silent." "")
+; (gtk_accel_path "<Actions>/Templates/Template Local" "")
+; (gtk_accel_path "<Actions>/Templates/Template T" "")
+; (gtk_accel_path "<Actions>/Tactics/Tactic reflexivity" "")
+; (gtk_accel_path "<Actions>/Templates/Template R" "")
+; (gtk_accel_path "<Actions>/Templates/Template Time" "")
+; (gtk_accel_path "<Actions>/Templates/Template P" "")
+; (gtk_accel_path "<Actions>/Tactics/Tactic decompose" "")
+; (gtk_accel_path "<Actions>/Templates/Template N" "")
+; (gtk_accel_path "<Actions>/Templates/Template Eval" "")
+; (gtk_accel_path "<Actions>/Tactics/Tactic congruence" "")
+; (gtk_accel_path "<Actions>/Templates/Template O" "")
+; (gtk_accel_path "<Actions>/Templates/Template E" "")
+; (gtk_accel_path "<Actions>/Templates/Template I" "")
+; (gtk_accel_path "<Actions>/Templates/Template H" "")
+; (gtk_accel_path "<Actions>/Templates/Template Extraction Language" "")
+; (gtk_accel_path "<Actions>/Templates/Template M" "")
+; (gtk_accel_path "<Actions>/Templates/Template Derive Inversion" "")
+; (gtk_accel_path "<Actions>/Tactics/Tactic double induction" "")
+; (gtk_accel_path "<Actions>/Templates/Template L" "")
+; (gtk_accel_path "<Actions>/Templates/Template Derive Inversion--clear" "")
+(gtk_accel_path "<Actions>/View/Display universe levels" "<Shift><Control>u")
+; (gtk_accel_path "<Actions>/Templates/Template G" "")
+; (gtk_accel_path "<Actions>/Templates/Template F" "")
+; (gtk_accel_path "<Actions>/Tactics/Tactic dependent inversion--clear -- with" "")
+; (gtk_accel_path "<Actions>/Templates/Template D" "")
+; (gtk_accel_path "<Actions>/Edit/Edit" "")
+; (gtk_accel_path "<Actions>/Tactics/Tactic firstorder" "")
+; (gtk_accel_path "<Actions>/Templates/Template C" "")
+(gtk_accel_path "<Actions>/Tactics/simpl" "<Primary><Control>s")
+; (gtk_accel_path "<Actions>/Tactics/Tactic replace -- with" "")
+; (gtk_accel_path "<Actions>/Templates/Template A" "")
+; (gtk_accel_path "<Actions>/Templates/Template Remove Printing Record" "")
+; (gtk_accel_path "<Actions>/Templates/Template Qed." "")
+; (gtk_accel_path "<Actions>/Templates/Template Program Fixpoint" "")
+(gtk_accel_path "<Actions>/View/Display coercions" "<Shift><Control>c")
+; (gtk_accel_path "<Actions>/Tactics/Tactic hnf" "")
+; (gtk_accel_path "<Actions>/Tactics/Tactic injection" "")
+; (gtk_accel_path "<Actions>/Tactics/Tactic rewrite" "")
+; (gtk_accel_path "<Actions>/Templates/Template Opaque" "")
+; (gtk_accel_path "<Actions>/Templates/Template Focus" "")
+; (gtk_accel_path "<Actions>/Templates/Template Ltac" "")
+; (gtk_accel_path "<Actions>/Tactics/Tactic simple destruct" "")
+(gtk_accel_path "<Actions>/View/Display all basic low-level contents" "<Shift><Control>a")
+; (gtk_accel_path "<Actions>/Tactics/Tactic jp <n>" "")
+; (gtk_accel_path "<Actions>/Templates/Template Test Printing Synth" "")
+; (gtk_accel_path "<Actions>/Tactics/Tactic set" "")
+; (gtk_accel_path "<Actions>/Edit/External editor" "")
+; (gtk_accel_path "<Actions>/View/Show Toolbar" "")
+(gtk_accel_path "<Actions>/Edit/Complete Word" "<Primary>slash")
+; (gtk_accel_path "<Actions>/Tactics/Tactic try" "")
+(gtk_accel_path "<Actions>/Templates/Fixpoint" "<Shift><Primary>f")
+; (gtk_accel_path "<Actions>/Tactics/Tactic discriminate" "")
+(gtk_accel_path "<Actions>/Navigation/Next" "<Primary><Control>greater")
+; (gtk_accel_path "<Actions>/Tactics/Tactic elimtype" "")
+; (gtk_accel_path "<Actions>/Templates/Template End" "")
+; (gtk_accel_path "<Actions>/Templates/Template Fixpoint" "")
+(gtk_accel_path "<Actions>/View/Next tab" "<Control>Right")
 ; (gtk_accel_path "<Actions>/File/File" "")
-; (gtk_accel_path "<DEFAULT ROOT>/D_erive Dependent Inversion__clear/" "")
-; (gtk_accel_path "<DEFAULT ROOT>/d_ecompose/" "")
-; (gtk_accel_path "<DEFAULT ROOT>/r_ewrite __ in/" "")
-(gtk_accel_path "<Actions>/Display/Display implicit arguments" "<Shift><Control>i")
-; (gtk_accel_path "<DEFAULT ROOT>/e_lim __ using/" "")
-; (gtk_accel_path "<DEFAULT ROOT>/a_ssert (__:=__)/" "")
-; (gtk_accel_path "<DEFAULT ROOT>/i_nversion __ using/" "")
-; (gtk_accel_path "<DEFAULT ROOT>/P_arameter/" "")
-; (gtk_accel_path "<DEFAULT ROOT>/H_int Constructors/" "")
-; (gtk_accel_path "<DEFAULT ROOT>/j_p <n>/" "")
-; (gtk_accel_path "<DEFAULT ROOT>/p_rogress/" "")
-; (gtk_accel_path "<CoqIde MenuBar>/Templates/_M.../" "")
-; (gtk_accel_path "<DEFAULT ROOT>/e_lim __ with/" "")
-; (gtk_accel_path "<DEFAULT ROOT>/f_irst/" "")
-; (gtk_accel_path "<DEFAULT ROOT>/l_azy/" "")
-; (gtk_accel_path "<DEFAULT ROOT>/i_nversion/" "")
-(gtk_accel_path "<Actions>/Help/Help for keyword" "<Meta>h")
-; (gtk_accel_path "<DEFAULT ROOT>/a_uto/" "")
-; (gtk_accel_path "<DEFAULT ROOT>/G_oal/" "")
-; (gtk_accel_path "<DEFAULT ROOT>/i_nversion __ using __ in/" "")
-(gtk_accel_path "<Actions>/Tactics/intuition" "<Meta><Control>i")
-; (gtk_accel_path "<DEFAULT ROOT>/r_ed in/" "")
-; (gtk_accel_path "<CoqIde MenuBar>/Tactics/_g.../" "")
-; (gtk_accel_path "<DEFAULT ROOT>/g_eneralize dependent/" "")
-; (gtk_accel_path "<Actions>/Queries/About" "F5")
-; (gtk_accel_path "<DEFAULT ROOT>/r_ight/" "")
-(gtk_accel_path "<Actions>/Tactics/auto" "<Meta><Control>a")
-(gtk_accel_path "<Actions>/Templates/Fixpoint" "<Shift><Meta>f")
-; (gtk_accel_path "<DEFAULT ROOT>/r_eflexivity/" "")
-; (gtk_accel_path "<DEFAULT ROOT>/i_nduction/" "")
-; (gtk_accel_path "<DEFAULT ROOT>/i_ntuition/" "")
-; (gtk_accel_path "<CoqIde MenuBar>/Tactics/_t.../" "")
-; (gtk_accel_path "<DEFAULT ROOT>/f_ix/" "")
-; (gtk_accel_path "<Actions>/Export/Pdf" "")
-; (gtk_accel_path "<DEFAULT ROOT>/N_ext Obligation/" "")
-(gtk_accel_path "<Actions>/Tactics/auto with *" "<Meta><Control>asterisk")
-; (gtk_accel_path "<DEFAULT ROOT>/R_ecord/" "")
-; (gtk_accel_path "<DEFAULT ROOT>/P_roof./" "")
-; (gtk_accel_path "<DEFAULT ROOT>/c_ontradiction/" "")
-; (gtk_accel_path "<DEFAULT ROOT>/S_et Extraction AutoInline/" "")
-; (gtk_accel_path "<DEFAULT ROOT>/e_auto/" "")
-; (gtk_accel_path "<DEFAULT ROOT>/d_ecompose record/" "")
-; (gtk_accel_path "<DEFAULT ROOT>/f_ield/" "")
-; (gtk_accel_path "<DEFAULT ROOT>/E_val/" "")
-; (gtk_accel_path "<DEFAULT ROOT>/R_eset Extraction Inline/" "")
+; (gtk_accel_path "<Actions>/Tactics/Tactic setoid--replace" "")
+; (gtk_accel_path "<Actions>/Tactics/Tactic generalize dependent" "")
+(gtk_accel_path "<Actions>/Tactics/trivial" "<Primary><Control>v")
+; (gtk_accel_path "<Actions>/Tactics/Tactic fix -- with" "")
+; (gtk_accel_path "<Actions>/Tactics/Tactic pose --:=--)" "")
+; (gtk_accel_path "<Actions>/Tactics/Tactic auto with" "")
+; (gtk_accel_path "<Actions>/Templates/Template Add Printing Record" "")
+; (gtk_accel_path "<Actions>/Tactics/Tactic inversion -- in" "")
+(gtk_accel_path "<Actions>/Tactics/eauto" "<Primary><Control>e")
+; (gtk_accel_path "<Actions>/File/Open" "<Primary>o")
+; (gtk_accel_path "<Actions>/Tactics/Tactic elim -- using" "")
+; (gtk_accel_path "<Actions>/Templates/Template Hint" "")
+; (gtk_accel_path "<Actions>/Tactics/Tactic tauto" "")
+; (gtk_accel_path "<Actions>/Export/Dvi" "")
+; (gtk_accel_path "<Actions>/Tactics/Tactic simpl -- in" "")
+; (gtk_accel_path "<Actions>/Templates/Template Hint Immediate" "")
diff --git a/ide/minilib.ml b/ide/minilib.ml
index 4ccb1ccb..74a42b23 100644
--- a/ide/minilib.ml
+++ b/ide/minilib.ml
@@ -79,48 +79,37 @@ let home =
 
 let opt2list = function None -> [] | Some x -> [x]
 
-let rec lconcat = function
-  | [] -> assert false
-  | [x] -> x
-  | x::l -> Filename.concat x (lconcat l)
+let (/) = Filename.concat
+
+let coqify d = d / "coq"
 
 let xdg_config_home =
-  try
-    Filename.concat (Sys.getenv "XDG_CONFIG_HOME") "coq"
-  with Not_found ->
-    lconcat [home;".config";"coq"]
+  coqify (try Sys.getenv "XDG_CONFIG_HOME" with Not_found -> home / ".config")
 
-let static_xdg_config_dirs =
-  if Sys.os_type = "Win32" then
-    let base = Filename.dirname (Filename.dirname Sys.executable_name) in
-    [Filename.concat base "config"]
-  else ["/etc/xdg/coq"]
+let relative_base =
+  Filename.dirname (Filename.dirname Sys.executable_name)
 
 let xdg_config_dirs =
-  xdg_config_home ::
-    try
-      List.map (fun dir -> Filename.concat dir "coq")
-	(path_to_list (Sys.getenv "XDG_CONFIG_DIRS"))
-    with Not_found -> static_xdg_config_dirs @ opt2list Coq_config.configdir
+  let sys_dirs =
+    try List.map coqify (path_to_list (Sys.getenv "XDG_CONFIG_DIRS"))
+    with
+      | Not_found when Sys.os_type = "Win32" -> [relative_base / "config"]
+      | Not_found -> ["/etc/xdg/coq"]
+  in
+  xdg_config_home :: sys_dirs @ opt2list Coq_config.configdir
 
 let xdg_data_home =
-  try
-    Filename.concat (Sys.getenv "XDG_DATA_HOME") "coq"
-  with Not_found ->
-    lconcat [home;".local";"share";"coq"]
-
-let static_xdg_data_dirs =
-  if Sys.os_type = "Win32" then
-    let base = Filename.dirname (Filename.dirname Sys.executable_name) in
-    [Filename.concat base "share"]
-  else ["/usr/local/share/coq";"/usr/share/coq"]
+  coqify
+    (try Sys.getenv "XDG_DATA_HOME" with Not_found -> home / ".local" / "share")
 
 let xdg_data_dirs =
-  xdg_data_home ::
-    try
-      List.map (fun dir -> Filename.concat dir "coq")
-	(path_to_list (Sys.getenv "XDG_DATA_DIRS"))
-    with Not_found -> static_xdg_data_dirs @ opt2list Coq_config.datadir
+  let sys_dirs =
+    try List.map coqify (path_to_list (Sys.getenv "XDG_DATA_DIRS"))
+    with
+      | Not_found when Sys.os_type = "Win32" -> [relative_base / "share"]
+      | Not_found -> ["/usr/local/share/coq";"/usr/share/coq"]
+  in
+  xdg_data_home :: sys_dirs @ opt2list Coq_config.datadir
 
 let coqtop_path = ref ""
 
diff --git a/ide/preferences.ml b/ide/preferences.ml
index d320ddda..17216b92 100644
--- a/ide/preferences.ml
+++ b/ide/preferences.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-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -279,7 +279,7 @@ let load_pref () =
     set_bool "auto_save" (fun v -> np.auto_save <- v);
     set_int "auto_save_delay" (fun v -> np.auto_save_delay <- v);
     set_pair "auto_save_name" (fun v1 v2 -> np.auto_save_name <- (v1,v2));
-    set_hd "encoding_manual" (fun v -> np.encoding <- (inputenc_of_string v));
+    set_hd "encoding" (fun v -> np.encoding <- (inputenc_of_string v));
     set_hd "project_options"
       (fun v -> np.read_project <- (project_behavior_of_string v));
     set_hd "project_file_name" (fun v -> np.project_file_name <- v);
diff --git a/ide/preferences.mli b/ide/preferences.mli
index b680c6f0..382aa091 100644
--- a/ide/preferences.mli
+++ b/ide/preferences.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-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/ide/project_file.ml4 b/ide/project_file.ml4
index 6bee0fec..aa1189ce 100644
--- a/ide/project_file.ml4
+++ b/ide/project_file.ml4
@@ -54,7 +54,7 @@ let rec process_cmd_line orig_dir ((project_file,makefile,install,opt) as opts)
     process_cmd_line orig_dir (project_file,makefile,install,true) l r
   | "-impredicative-set" :: r ->
     Minilib.safe_prerr_endline "Please now use \"-arg -impredicative-set\" instead of \"-impredicative-set\" alone to be more uniform.";
-    process_cmd_line orig_dir opts (Arg "-impredicative_set" :: l) r
+    process_cmd_line orig_dir opts (Arg "-impredicative-set" :: l) r
   | "-no-install" :: r ->
     Minilib.safe_prerr_endline "Option -no-install is deprecated. Use \"-install none\" instead";
     process_cmd_line orig_dir (project_file,makefile,NoInstall,opt) l r
diff --git a/ide/tags.ml b/ide/tags.ml
index eeace465..7b67944b 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-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/ide/tags.mli b/ide/tags.mli
index 53a8c493..36f18a2f 100644
--- a/ide/tags.mli
+++ b/ide/tags.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-2012     *)
 (*   \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 499d56bd..60c89eb1 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-2012     *)
 (*   \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 57724297..0951ab5e 100644
--- a/ide/undo.ml
+++ b/ide/undo.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-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/ide/undo_lablgtk_ge212.mli b/ide/undo_lablgtk_ge212.mli
index d9451fd1..95168b17 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-2012     *)
 (*   \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 a2eb65bd..4b471395 100644
--- a/ide/undo_lablgtk_ge26.mli
+++ b/ide/undo_lablgtk_ge26.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-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/ide/undo_lablgtk_lt26.mli b/ide/undo_lablgtk_lt26.mli
index b193007b..df76ee5e 100644
--- a/ide/undo_lablgtk_lt26.mli
+++ b/ide/undo_lablgtk_lt26.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-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/ide/utf8_convert.mll b/ide/utf8_convert.mll
index d29ae0bd..f27f96a6 100644
--- a/ide/utf8_convert.mll
+++ b/ide/utf8_convert.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-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)