diff options
Diffstat (limited to 'ide')
-rw-r--r-- | ide/command_windows.ml | 2 | ||||
-rw-r--r-- | ide/command_windows.mli | 2 | ||||
-rw-r--r-- | ide/config_lexer.mll | 2 | ||||
-rw-r--r-- | ide/coq.ml | 2 | ||||
-rw-r--r-- | ide/coq.mli | 2 | ||||
-rw-r--r-- | ide/coq_commands.ml | 2 | ||||
-rw-r--r-- | ide/coq_lex.mll | 2 | ||||
-rw-r--r-- | ide/coqide.ml | 13 | ||||
-rw-r--r-- | ide/coqide.mli | 2 | ||||
-rw-r--r-- | ide/coqide_main.ml4 | 2 | ||||
-rw-r--r-- | ide/gtk_parsing.ml | 2 | ||||
-rw-r--r-- | ide/ide_mac_stubs.c | 10 | ||||
-rw-r--r-- | ide/ideproof.ml | 40 | ||||
-rw-r--r-- | ide/ideutils.ml | 2 | ||||
-rw-r--r-- | ide/ideutils.mli | 2 | ||||
-rw-r--r-- | ide/mac_default_accel_map | 726 | ||||
-rw-r--r-- | ide/minilib.ml | 55 | ||||
-rw-r--r-- | ide/preferences.ml | 4 | ||||
-rw-r--r-- | ide/preferences.mli | 2 | ||||
-rw-r--r-- | ide/project_file.ml4 | 2 | ||||
-rw-r--r-- | ide/tags.ml | 2 | ||||
-rw-r--r-- | ide/tags.mli | 2 | ||||
-rw-r--r-- | ide/typed_notebook.ml | 2 | ||||
-rw-r--r-- | ide/undo.ml | 2 | ||||
-rw-r--r-- | ide/undo_lablgtk_ge212.mli | 2 | ||||
-rw-r--r-- | ide/undo_lablgtk_ge26.mli | 2 | ||||
-rw-r--r-- | ide/undo_lablgtk_lt26.mli | 2 | ||||
-rw-r--r-- | ide/utf8_convert.mll | 2 |
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 *) @@ -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 *) |