From daf719e5554e823b6540be05e48e96ac478e2865 Mon Sep 17 00:00:00 2001 From: pboutill Date: Fri, 27 Apr 2012 16:43:30 +0000 Subject: Coqide MacOS integration refresh git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15254 85f007b7-540e-0410-9357-904b9bb8a0f7 --- configure | 6 +- dev/macosify_accel.sh | 3 + ide/coqide.ml | 6 +- ide/ide_mac_stubs.c | 10 +- ide/mac_default_accel_map | 729 +++++++++++++++++++++++----------------------- 5 files changed, 382 insertions(+), 372 deletions(-) create mode 100755 dev/macosify_accel.sh diff --git a/configure b/configure index 85b97b73b1..94268c7a39 100755 --- a/configure +++ b/configure @@ -656,10 +656,10 @@ else else echo "LablGtk2 found, native threads: native CoqIde will be available." COQIDE=opt - if [ "$nomacintegration_spec" = "no" ] && pkg-config --exists ige-mac-integration; + if [ "$nomacintegration_spec" = "no" ] && pkg-config --exists gtk-mac-integration; then - cflags=$cflags" `pkg-config --cflags ige-mac-integration`" - IDEARCHFLAGS='-ccopt "`pkg-config --libs ige-mac-integration`"' + cflags=$cflags" `pkg-config --cflags gtk-mac-integration`" + IDEARCHFLAGS='-ccopt "`pkg-config --libs gtk-mac-integration`"' IDEARCHFILE=ide/ide_mac_stubs.o IDEARCHDEF=QUARTZ elif [ "$ARCH" = "win32" ]; diff --git a/dev/macosify_accel.sh b/dev/macosify_accel.sh new file mode 100755 index 0000000000..23c557f082 --- /dev/null +++ b/dev/macosify_accel.sh @@ -0,0 +1,3 @@ +#!/usr/bin/sed -f +s/^;\{0,1\} *\(.*\)\(.*\)$/\1\2/ +s/^;\{0,1\} *\(.*\)\(.*\)$/\1\2/ diff --git a/ide/coqide.ml b/ide/coqide.ml index afa8ea71c5..2ecf524cbf 100644 --- a/ide/coqide.ml +++ b/ide/coqide.ml @@ -2229,13 +2229,13 @@ let main files = session_notebook#current_term.script#as_view ~sgn:GtkText.View.S.paste_clipboard with _ -> prerr_endline "EMIT PASTE FAILED") ~stock:`PASTE; - GAction.add_action "Find" ~label:"_Find" ~stock:`FIND ~accel:"F" + GAction.add_action "Find" ~stock:`FIND ~callback:(fun _ -> session_notebook#current_term.finder#show_find ()); GAction.add_action "Find Next" ~label:"Find _Next" ~stock:`GO_DOWN ~accel:"F3" ~callback:(fun _ -> session_notebook#current_term.finder#find_forward ()); GAction.add_action "Find Previous" ~label:"Find _Previous" ~stock:`GO_UP ~accel:"F3" ~callback:(fun _ -> session_notebook#current_term.finder#find_backward ()); - GAction.add_action "Replace" ~label:"_Replace" ~stock:`FIND_AND_REPLACE ~accel:"R" + GAction.add_action "Replace" ~stock:`FIND_AND_REPLACE ~callback:(fun _ -> session_notebook#current_term.finder#show_replace ()); GAction.add_action "Close Find" ~accel:"Escape" ~callback:(fun _ -> session_notebook#current_term.finder#hide ()); @@ -2258,7 +2258,7 @@ 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:"," ~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"; diff --git a/ide/ide_mac_stubs.c b/ide/ide_mac_stubs.c index 64deb71d07..2aeb2bf42f 100644 --- a/ide/ide_mac_stubs.c +++ b/ide/ide_mac_stubs.c @@ -8,7 +8,7 @@ #include #include #include -#include +#include 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/mac_default_accel_map b/ide/mac_default_accel_map index e570ae6512..28ff7b9a9f 100644 --- a/ide/mac_default_accel_map +++ b/ide/mac_default_accel_map @@ -1,372 +1,379 @@ -; coqide.opt GtkAccelMap rc-file -*- scheme -*- +; coqide GtkAccelMap rc-file -*- scheme -*- ; this file is an automated accelerator map dump ; -; (gtk_accel_path "/C_anonical Structure/" "") -; (gtk_accel_path "/M_odule Type/" "") -; (gtk_accel_path "/c_ompute/" "") -; (gtk_accel_path "/Templates/_E.../" "") -(gtk_accel_path "/Templates/match" "c") -; (gtk_accel_path "/D_erive Inversion/" "") -; (gtk_accel_path "/Queries/Check" "F3") -; (gtk_accel_path "/i_dtac/" "") -; (gtk_accel_path "/L_oad/" "") -; (gtk_accel_path "/a_ssert/" "") -; (gtk_accel_path "/f_irstorder using/" "") -; (gtk_accel_path "/s_olve/" "") -; (gtk_accel_path "/Tactics/_l.../" "") -(gtk_accel_path "/Templates/Inductive" "i") -; (gtk_accel_path "/a_ssert (__:__)/" "") -; (gtk_accel_path "/T_est Printing Synth/" "") -; (gtk_accel_path "/Templates/_R.../" "") -; (gtk_accel_path "/Help/Browse Coq Library" "") -; (gtk_accel_path "/U_nset Extraction Optimize/" "") -; (gtk_accel_path "/s_imple inversion/" "") -(gtk_accel_path "/Edit/Copy" "c") -; (gtk_accel_path "/E_xtract Inductive/" "") -(gtk_accel_path "/Edit/Cut" "x") -; (gtk_accel_path "/i_nfo/" "") -; (gtk_accel_path "/R_emove Printing If/" "") -; (gtk_accel_path "/e_apply/" "") -; (gtk_accel_path "/F_ixpoint/" "") -; (gtk_accel_path "/c_hange __ in/" "") -; (gtk_accel_path "/l_apply/" "") -; (gtk_accel_path "/s_imple induction/" "") -; (gtk_accel_path "/f_ail/" "") -; (gtk_accel_path "/e_lim/" "") -; (gtk_accel_path "/r_ewrite <- __ in/" "") -; (gtk_accel_path "/A_dd Printing Let/" "") -; (gtk_accel_path "/T_ransparent/" "") -; (gtk_accel_path "/Tactics/_d.../" "") -(gtk_accel_path "/Tactics/Wizard" "dollar") +; (gtk_accel_path "/Templates/Template Read Module" "") +; (gtk_accel_path "/Tactics/Tactic pattern" "") +(gtk_accel_path "/Templates/Definition" "d") +; (gtk_accel_path "/Templates/Template Program Lemma" "") +(gtk_accel_path "/Templates/Lemma" "l") +; (gtk_accel_path "/Templates/Template Fact" "") +(gtk_accel_path "/Tactics/auto" "a") +; (gtk_accel_path "/Tactics/Tactic fold" "") +; (gtk_accel_path "/Help/About Coq" "") +; (gtk_accel_path "/Templates/Template Add Ring A Aplus Amult Aone Azero Ainv Aeq T [ c1 ... cn ]. " "") +; (gtk_accel_path "/Templates/Template Hypothesis" "") +; (gtk_accel_path "/Tactics/Tactic repeat" "") +; (gtk_accel_path "/Templates/Template Unset Extraction Optimize" "") +; (gtk_accel_path "/Templates/Template Add Printing Constructor" "") ; (gtk_accel_path "/Windows/Detach View" "") -; (gtk_accel_path "/T_heorem/" "") -(gtk_accel_path "/Templates/Scheme" "s") -; (gtk_accel_path "/R_emark/" "") -; (gtk_accel_path "/Compile/Compile" "") -; (gtk_accel_path "/A_dd Relation/" "") -; (gtk_accel_path "/r_ename __ into/" "") -; (gtk_accel_path "/File/Save as" "") -; (gtk_accel_path "/f_irstorder/" "") -; (gtk_accel_path "/G_rammar/" "") -; (gtk_accel_path "/f_irstorder with/" "") -; (gtk_accel_path "/r_ed/" "") -; (gtk_accel_path "/D_efinition/" "") -; (gtk_accel_path "/R_equire Import/" "") -; (gtk_accel_path "/d_iscriminate/" "") -; (gtk_accel_path "/i_ntro after/" "") -; (gtk_accel_path "/Export/Latex" "") -; (gtk_accel_path "/j_p/" "") -; (gtk_accel_path "/a_uto with/" "") -; (gtk_accel_path "/S_ection/" "") -; (gtk_accel_path "/r_ewrite/" "") -; (gtk_accel_path "/Export/Html" "") -; (gtk_accel_path "/Tactics/_i.../" "") -; (gtk_accel_path "/a_utorewrite/" "") -; (gtk_accel_path "/F_ocus/" "") -; (gtk_accel_path "/Templates/_O.../" "") -; (gtk_accel_path "/l_azy in/" "") -; (gtk_accel_path "/d_ependent inversion__clear __ with/" "") -; (gtk_accel_path "/c_utrewrite/" "") -(gtk_accel_path "/Edit/Undo" "u") -; (gtk_accel_path "/c_onstructor __ with/" "") -; (gtk_accel_path "/r_ing/" "") -; (gtk_accel_path "/d_ependent rewrite <-/" "") -; (gtk_accel_path "/e_limtype/" "") -(gtk_accel_path "/Tactics/simpl" "s") -; (gtk_accel_path "/H_int/" "") -; (gtk_accel_path "/H_int Rewrite/" "") -; (gtk_accel_path "/V_ariable/" "") -; (gtk_accel_path "/U_nset Implicit Arguments/" "") -; (gtk_accel_path "/s_implify__eq/" "") -; (gtk_accel_path "/Compile/Next error" "F7") -; (gtk_accel_path "/Edit/Edit" "") -; (gtk_accel_path "/S_et Extraction Optimize/" "") -; (gtk_accel_path "/H_ypothesis/" "") -; (gtk_accel_path "/E_nd Silent./" "") -; (gtk_accel_path "/S_yntax/" "") -; (gtk_accel_path "/d_ecide equality/" "") -; (gtk_accel_path "/O_paque/" "") -; (gtk_accel_path "/Templates/_T.../" "") -; (gtk_accel_path "/Tactics/_a.../" "") -; (gtk_accel_path "/Templates/_G.../" "") -; (gtk_accel_path "/c_ase/" "") -(gtk_accel_path "/Navigation/Backward" "Up") -; (gtk_accel_path "/C_oFixpoint/" "") -; (gtk_accel_path "/P_rogram Fixpoint/" "") -; (gtk_accel_path "/d_ependent inversion__clear/" "") -; (gtk_accel_path "/c_ase __ with/" "") -; (gtk_accel_path "/a_ssumption/" "") -; (gtk_accel_path "/t_ransitivity/" "") -; (gtk_accel_path "/i_ntros until/" "") -; (gtk_accel_path "/s_plit/" "") -; (gtk_accel_path "/e_xists/" "") -(gtk_accel_path "/Templates/Theorem" "t") -; (gtk_accel_path "/Navigation/Navigation" "") -; (gtk_accel_path "/H_int Unfold/" "") -; (gtk_accel_path "/I_mplicit Arguments/" "") -; (gtk_accel_path "/Help/Help" "") -; (gtk_accel_path "/d_ecompose sum/" "") -; (gtk_accel_path "/A_dd Abstract Ring A Aplus Amult Aone Azero Ainv Aeq T./" "") -; (gtk_accel_path "/Te_mplates/" "") -(gtk_accel_path "/Edit/Find" "f") -; (gtk_accel_path "/r_eplace __ with/" "") -(gtk_accel_path "/Tactics/omega" "o") -; (gtk_accel_path "/S_cheme/" "") -; (gtk_accel_path "/L_emma/" "") -; (gtk_accel_path "/i_nversion__clear __ in/" "") -; (gtk_accel_path "/E_xtraction Inline/" "") -; (gtk_accel_path "/S_yntactic Definition/" "") -; (gtk_accel_path "/i_nstantiate (__:=__)/" "") -; (gtk_accel_path "/C_hapter/" "") -; (gtk_accel_path "/Templates/_L.../" "") -; (gtk_accel_path "/Tactics/_f.../" "") -; (gtk_accel_path "/Queries/Queries" "") -; (gtk_accel_path "/T_est Printing Wildcard/" "") -(gtk_accel_path "/File/Open" "o") -; (gtk_accel_path "/f_old __ in/" "") -(gtk_accel_path "/Navigation/Go to" "Right") +; (gtk_accel_path "/Tactics/Tactic inversion" "") +; (gtk_accel_path "/Templates/Template Write State" "") ; (gtk_accel_path "/Export/Export to" "") -; (gtk_accel_path "/c_ongruence/" "") -; (gtk_accel_path "/c_learbody/" "") -(gtk_accel_path "/File/Close buffer" "w") -; (gtk_accel_path "/a_pply/" "") -; (gtk_accel_path "/Queries/SearchAbout" "F2") -; (gtk_accel_path "/i_ntro/" "") -; (gtk_accel_path "/H_int Immediate/" "") -; (gtk_accel_path "/p_ose __:=__)/" "") -; (gtk_accel_path "/U_nset Undo/" "") -; (gtk_accel_path "/Tactics/_s.../" "") -; (gtk_accel_path "/P_rogram Definition/" "") -; (gtk_accel_path "/R_equire/" "") -; (gtk_accel_path "/c_ompare/" "") -; (gtk_accel_path "/s_ymmetry in/" "") -(gtk_accel_path "/Display/Display coercions" "c") -(gtk_accel_path "/Navigation/Previous" "less") -(gtk_accel_path "/Display/Display all low-level contents" "l") -; (gtk_accel_path "/C_oercion Local/" "") -; (gtk_accel_path "/f_ix __ with/" "") -; (gtk_accel_path "/A_dd ML Path/" "") -; (gtk_accel_path "/A_xiom/" "") -; (gtk_accel_path "/Templates/Templates" "") -; (gtk_accel_path "/a_bstract/" "") -; (gtk_accel_path "/Edit/Clear Undo Stack" "") -(gtk_accel_path "/File/New" "n") -; (gtk_accel_path "/Tactics/_hnf/" "") -; (gtk_accel_path "/d_o/" "") -; (gtk_accel_path "/E_xtract Constant/" "") -; (gtk_accel_path "/E_nd/" "") -; (gtk_accel_path "/Templates/_Qed./" "") -; (gtk_accel_path "/A_dd Rec ML Path/" "") -; (gtk_accel_path "/Templates/_D.../" "") -(gtk_accel_path "/Navigation/Hide" "h") -; (gtk_accel_path "/c_ofix/" "") -; (gtk_accel_path "/_Try Tactics/" "") -; (gtk_accel_path "/S_et Printing Wildcard/" "") -; (gtk_accel_path "/i_nversion__clear/" "") -; (gtk_accel_path "/Templates/_V.../" "") +(gtk_accel_path "/Tactics/auto with *" "asterisk") +; (gtk_accel_path "/Tactics/Tactic inversion--clear" "") +; (gtk_accel_path "/Templates/Template Implicit Arguments" "") +; (gtk_accel_path "/Edit/Copy" "c") +; (gtk_accel_path "/Tactics/Tactic inversion -- using" "") +; (gtk_accel_path "/View/Previous tab" "Left") +; (gtk_accel_path "/Tactics/Tactic change -- in" "") +; (gtk_accel_path "/Tactics/Tactic jp" "") +; (gtk_accel_path "/Tactics/Tactic red" "") +; (gtk_accel_path "/Templates/Template Coercion" "") +; (gtk_accel_path "/Templates/Template CoFixpoint" "") +; (gtk_accel_path "/Tactics/Tactic intros until" "") +; (gtk_accel_path "/Templates/Template Derive Dependent Inversion" "") +; (gtk_accel_path "/Tactics/Tactic eapply" "") +; (gtk_accel_path "/View/View" "") +; (gtk_accel_path "/Tactics/Tactic change" "") +; (gtk_accel_path "/Tactics/Tactic firstorder using" "") +; (gtk_accel_path "/Tactics/Tactic decompose sum" "") +; (gtk_accel_path "/Tactics/Tactic cut" "") +; (gtk_accel_path "/Templates/Template Remove Printing Let" "") +; (gtk_accel_path "/Templates/Template Structure" "") +; (gtk_accel_path "/Tactics/Tactic compute in" "") +; (gtk_accel_path "/Queries/Locate" "") +; (gtk_accel_path "/Templates/Template Save." "") +; (gtk_accel_path "/Templates/Template Canonical Structure" "") +; (gtk_accel_path "/Tactics/Tactic compare" "") +; (gtk_accel_path "/Templates/Template Next Obligation" "") +(gtk_accel_path "/View/Display notations" "n") +; (gtk_accel_path "/Tactics/Tactic fail" "") +; (gtk_accel_path "/Tactics/Tactic left" "") +(gtk_accel_path "/Edit/Undo" "u") +(gtk_accel_path "/Tactics/eauto with *" "ampersand") +; (gtk_accel_path "/Templates/Template Infix" "") +; (gtk_accel_path "/Tactics/Tactic functional induction" "") +; (gtk_accel_path "/Tactics/Tactic clear" "") +; (gtk_accel_path "/Templates/Template End Silent." "") +; (gtk_accel_path "/Tactics/Tactic intros" "") +; (gtk_accel_path "/Tactics/Tactic constructor -- with" "") +; (gtk_accel_path "/Tactics/Tactic destruct" "") +; (gtk_accel_path "/Tactics/Tactic intro after" "") +; (gtk_accel_path "/Tactics/Tactic abstract" "") +; (gtk_accel_path "/Compile/Compile buffer" "") +; (gtk_accel_path "/Queries/About" "F5") +; (gtk_accel_path "/Templates/Template CoInductive" "") +; (gtk_accel_path "/Templates/Template Test Printing Wildcard" "") +; (gtk_accel_path "/Templates/Template Unset Hyps--limit" "") +; (gtk_accel_path "/Templates/Template Transparent" "") ; (gtk_accel_path "/Export/Ps" "") -; (gtk_accel_path "/U_nset Hyps__limit/" "") -; (gtk_accel_path "/H_int Extern/" "") -; (gtk_accel_path "/f_unctional induction/" "") -; (gtk_accel_path "/U_nset Extraction AutoInline/" "") -; (gtk_accel_path "/U_nfocus/" "") -; (gtk_accel_path "/Edit/External editor" "") -; (gtk_accel_path "/I_dentity Coercion/" "") -; (gtk_accel_path "/a_bsurd/" "") -; (gtk_accel_path "/c_hange/" "") -(gtk_accel_path "/Tactics/eauto" "e") -; (gtk_accel_path "/O_bligations Tactic/" "") -(gtk_accel_path "/Tactics/trivial" "v") -; (gtk_accel_path "/d_ependent inversion/" "") -; (gtk_accel_path "/c_bv/" "") -; (gtk_accel_path "/A_dd Ring A Aplus Amult Aone Azero Ainv Aeq T [ c1 ... cn ]. /" "") -; (gtk_accel_path "/p_ose/" "") -; (gtk_accel_path "/s_et (__:=__)/" "") -; (gtk_accel_path "/R_equire Export/" "") -; (gtk_accel_path "/L_tac/" "") -; (gtk_accel_path "/A_dd Rec LoadPath/" "") -; (gtk_accel_path "/Tactics/_c.../" "") -(gtk_accel_path "/Navigation/End" "End") -(gtk_accel_path "/Templates/Lemma" "l") -(gtk_accel_path "/Navigation/Start" "Home") -; (gtk_accel_path "/Templates/_I.../" "") -(gtk_accel_path "/File/Print..." "p") -; (gtk_accel_path "/d_ependent rewrite ->/" "") -; (gtk_accel_path "/S_tructure/" "") -; (gtk_accel_path "/T_est Printing Let/" "") -; (gtk_accel_path "/T_ime/" "") -; (gtk_accel_path "/g_eneralize/" "") -(gtk_accel_path "/Display/Display all basic low-level contents" "a") -; (gtk_accel_path "/Tactics/_p.../" "") -; (gtk_accel_path "/f_old/" "") -; (gtk_accel_path "/H_int Resolve/" "") -; (gtk_accel_path "/M_utual Inductive/" "") -; (gtk_accel_path "/i_nversion __ in/" "") -; (gtk_accel_path "/Windows/Show/Hide Toolbar" "") -(gtk_accel_path "/File/Save" "s") -; (gtk_accel_path "/File/Save all" "") -; (gtk_accel_path "/Queries/Print" "F4") -; (gtk_accel_path "/c_onstructor/" "") -; (gtk_accel_path "/Export/Dvi" "") -; (gtk_accel_path "/s_etoid__replace/" "") -; (gtk_accel_path "/D_efined./" "") -; (gtk_accel_path "/I_nfix/" "") -(gtk_accel_path "/Navigation/Next" "greater") -; (gtk_accel_path "/A_dd Morphism/" "") +; (gtk_accel_path "/Tactics/Tactic elim" "") +; (gtk_accel_path "/Templates/Template Extract Constant" "") +; (gtk_accel_path "/Tactics/Tactic assert (--:--)" "") +; (gtk_accel_path "/Templates/Template Add Rec LoadPath" "") +; (gtk_accel_path "/Edit/Redo" "") +; (gtk_accel_path "/Tactics/Tactic compute" "") +; (gtk_accel_path "/Compile/Next error" "F7") +; (gtk_accel_path "/Templates/Template Add ML Path" "") +; (gtk_accel_path "/Templates/Template Test Printing If" "") +; (gtk_accel_path "/Templates/Template Load Verbose" "") +; (gtk_accel_path "/Templates/Template Reset Extraction Inline" "") +; (gtk_accel_path "/Templates/Template Set Implicit Arguments" "") +; (gtk_accel_path "/Templates/Template Test Printing Let" "") ; (gtk_accel_path "/Windows/Windows" "") -; (gtk_accel_path "/e_xact/" "") -; (gtk_accel_path "/c_bv in/" "") -; (gtk_accel_path "/t_ry/" "") -; (gtk_accel_path "/Templates/_A.../" "") -(gtk_accel_path "/Display/Display notations" "n") -; (gtk_accel_path "/c_lear/" "") +; (gtk_accel_path "/Templates/Template Defined." "") +(gtk_accel_path "/Templates/match" "c") +; (gtk_accel_path "/Tactics/Tactic set (--:=--)" "") +; (gtk_accel_path "/Templates/Template Proof." "") ; (gtk_accel_path "/Compile/Make" "F6") -(gtk_accel_path "/Tactics/eauto with *" "ampersand") -; (gtk_accel_path "/Help/Browse Coq Manual" "") -; (gtk_accel_path "/Templates/_N.../" "") -(gtk_accel_path "/File/Quit" "q") -; (gtk_accel_path "/u_nfold/" "") -; (gtk_accel_path "/Tactics/_u.../" "") -; (gtk_accel_path "/d_ouble induction/" "") -; (gtk_accel_path "/S_et Silent./" "") -; (gtk_accel_path "/V_ariables/" "") -; (gtk_accel_path "/U_nset Printing Wildcard/" "") -; (gtk_accel_path "/r_ewrite <-/" "") -; (gtk_accel_path "/I_nductive/" "") -; (gtk_accel_path "/e_auto with/" "") -; (gtk_accel_path "/r_epeat/" "") -; (gtk_accel_path "/Queries/Locate" "") -; (gtk_accel_path "/S_et Hyps__limit/" "") -; (gtk_accel_path "/A_dd Abstract Semi Ring A Aplus Amult Aone Azero Aeq T./" "") -; (gtk_accel_path "/c_ompute in/" "") -; (gtk_accel_path "/Templates/_F.../" "") -; (gtk_accel_path "/G_lobal Variable/" "") -; (gtk_accel_path "/t_auto/" "") -; (gtk_accel_path "/E_xtraction NoInline/" "") -; (gtk_accel_path "/u_nfold __ in/" "") -; (gtk_accel_path "/s_imple destruct/" "") -(gtk_accel_path "/Navigation/Interrupt" "Break") -; (gtk_accel_path "/Templates/_S.../" "") -; (gtk_accel_path "/i_njection/" "") -; (gtk_accel_path "/R_ead Module/" "") -; (gtk_accel_path "/P_rogram Lemma/" "") -; (gtk_accel_path "/U_nset Silent./" "") -(gtk_accel_path "/Display/Display universe levels" "u") -; (gtk_accel_path "/f_ourier/" "") -; (gtk_accel_path "/D_erive Inversion__clear/" "") -; (gtk_accel_path "/Tactics/_omega/" "") -; (gtk_accel_path "/S_et Undo/" "") -; (gtk_accel_path "/A_dd Semi Ring A Aplus Amult Aone Azero Aeq T [ c1 ... cn ]./" "") -; (gtk_accel_path "/s_impl __ in/" "") -; (gtk_accel_path "/Windows/Show/Hide Query Pane" "Escape") -; (gtk_accel_path "/R_estore State/" "") -; (gtk_accel_path "/R_emove Printing Let/" "") -; (gtk_accel_path "/A_dd Printing If/" "") -(gtk_accel_path "/Tactics/tauto" "p") -; (gtk_accel_path "/s_impl/" "") -; (gtk_accel_path "/i_ntros/" "") -; (gtk_accel_path "/s_ymmetry/" "") -; (gtk_accel_path "/c_ut/" "") -; (gtk_accel_path "/r_efine/" "") -; (gtk_accel_path "/Tactics/_e.../" "") -; (gtk_accel_path "/e_exact/" "") -(gtk_accel_path "/Navigation/Forward" "Down") -(gtk_accel_path "/Edit/Paste" "v") -; (gtk_accel_path "/C_oercion/" "") -; (gtk_accel_path "/Tactics/_r.../" "") -; (gtk_accel_path "/d_estruct/" "") -; (gtk_accel_path "/A_dd Setoid/" "") -; (gtk_accel_path "/Queries/Whelp Locate" "") -; (gtk_accel_path "/T_est Printing If/" "") -; (gtk_accel_path "/Display/Display" "") -; (gtk_accel_path "/Tactics/_move __ after/" "") -(gtk_accel_path "/Edit/Complete Word" "slash") -; (gtk_accel_path "/s_ubst/" "") -; (gtk_accel_path "/Help/About Coq" "") -; (gtk_accel_path "/s_etoid__rewrite/" "") +; (gtk_accel_path "/Templates/Template Module Type" "") +; (gtk_accel_path "/Tactics/Tactic apply -- with" "") +; (gtk_accel_path "/File/Save as" "") +; (gtk_accel_path "/Templates/Template Set Hyps--limit" "") +; (gtk_accel_path "/Templates/Template Global Variable" "") +; (gtk_accel_path "/Templates/Template Remove Printing Constructor" "") +; (gtk_accel_path "/Templates/Template Add Setoid" "") +; (gtk_accel_path "/Edit/Find Next" "F3") +; (gtk_accel_path "/Edit/Find" "f") +; (gtk_accel_path "/Templates/Template Add Relation" "") +; (gtk_accel_path "/Queries/Print" "F4") +; (gtk_accel_path "/Templates/Template Obligations Tactic" "") +; (gtk_accel_path "/Tactics/Tactic trivial" "") +; (gtk_accel_path "/Tactics/Tactic first" "") +; (gtk_accel_path "/Tactics/Tactic case" "") +; (gtk_accel_path "/Templates/Template Hint Constructors" "") +; (gtk_accel_path "/Templates/Template Add Abstract Ring A Aplus Amult Aone Azero Ainv Aeq T." "") +; (gtk_accel_path "/Templates/Template Coercion Local" "") +(gtk_accel_path "/View/Show Query Pane" "Escape") +; (gtk_accel_path "/Tactics/Tactic cbv" "") +; (gtk_accel_path "/Tactics/Tactic inversion--clear -- in" "") +; (gtk_accel_path "/Templates/Template Add Rec ML Path" "") +; (gtk_accel_path "/Tactics/Tactic apply" "") +; (gtk_accel_path "/Export/Latex" "") +; (gtk_accel_path "/Tactics/Tactic inversion -- using -- in" "") +; (gtk_accel_path "/Tactics/Tactic generalize" "") +(gtk_accel_path "/Navigation/Backward" "Up") +; (gtk_accel_path "/Tactics/Tactic p" "") +(gtk_accel_path "/Navigation/Hide" "h") +; (gtk_accel_path "/File/Close buffer" "w") +; (gtk_accel_path "/Tactics/Tactic induction" "") +; (gtk_accel_path "/Tactics/Tactic eauto with" "") +(gtk_accel_path "/View/Display raw matching expressions" "m") +; (gtk_accel_path "/Tactics/Tactic d" "") +; (gtk_accel_path "/Tactics/Tactic u" "") +; (gtk_accel_path "/Templates/Templates" "") +; (gtk_accel_path "/Tactics/Tactic s" "") +; (gtk_accel_path "/Tactics/Tactic lapply" "") +; (gtk_accel_path "/Tactics/Tactic t" "") +; (gtk_accel_path "/Tactics/Tactic r" "") +; (gtk_accel_path "/Edit/Replace" "r") +; (gtk_accel_path "/Tactics/Tactic case -- with" "") +; (gtk_accel_path "/Tactics/Tactic eexact" "") +; (gtk_accel_path "/Queries/Check" "F3") +; (gtk_accel_path "/Tactics/Tactic omega" "") +; (gtk_accel_path "/File/New" "n") +; (gtk_accel_path "/Tactics/Tactic l" "") +; (gtk_accel_path "/Tactics/Tactic intro" "") +; (gtk_accel_path "/Tactics/Tactic j" "") +; (gtk_accel_path "/Tactics/Tactic i" "") +; (gtk_accel_path "/Templates/Template Definition" "") +; (gtk_accel_path "/Tactics/Tactic g" "") +; (gtk_accel_path "/Tactics/Tactic f" "") +; (gtk_accel_path "/Tactics/Tactic e" "") +; (gtk_accel_path "/Tactics/Tactic c" "") +(gtk_accel_path "/File/Rehighlight" "l") +; (gtk_accel_path "/Tactics/Tactic simple inversion" "") +; (gtk_accel_path "/Tactics/Tactic a" "") +; (gtk_accel_path "/Templates/Template Mutual Inductive" "") +; (gtk_accel_path "/Templates/Template Extraction NoInline" "") +(gtk_accel_path "/Templates/Theorem" "t") +; (gtk_accel_path "/Templates/Template Derive Dependent Inversion--clear" "") +; (gtk_accel_path "/Tactics/Tactic unfold" "") ; (gtk_accel_path "/Tactics/Try Tactics" "") -; (gtk_accel_path "/Templates/_C.../" "") -; (gtk_accel_path "/L_ocal/" "") -; (gtk_accel_path "/s_et/" "") -; (gtk_accel_path "/Tactics/_quote/" "") -(gtk_accel_path "/Templates/Definition" "d") -; (gtk_accel_path "/S_et Implicit Arguments/" "") +; (gtk_accel_path "/Tactics/Tactic red in" "") +; (gtk_accel_path "/Tactics/Tactic rewrite <- -- in" "") +; (gtk_accel_path "/Templates/Template Hint Extern" "") +; (gtk_accel_path "/Templates/Template Unfocus" "") +; (gtk_accel_path "/Tactics/Tactic dependent inversion--clear" "") +; (gtk_accel_path "/Help/Browse Coq Library" "") +; (gtk_accel_path "/Tactics/Tactic lazy" "") +; (gtk_accel_path "/Templates/Template Scheme" "") +(gtk_accel_path "/Tactics/tauto" "p") +; (gtk_accel_path "/Tactics/Tactic cutrewrite" "") +; (gtk_accel_path "/Tactics/Tactic contradiction" "") +; (gtk_accel_path "/Templates/Template Set Printing Wildcard" "") +; (gtk_accel_path "/Templates/Template Add LoadPath" "") +(gtk_accel_path "/Navigation/Previous" "less") +; (gtk_accel_path "/Templates/Template Require" "") +; (gtk_accel_path "/Tactics/Tactic simpl" "") +; (gtk_accel_path "/Templates/Template Require Import" "") +; (gtk_accel_path "/Templates/Template Add Abstract Semi Ring A Aplus Amult Aone Azero Aeq T." "") +(gtk_accel_path "/Navigation/Forward" "Down") +; (gtk_accel_path "/Tactics/Tactic rename -- into" "") +; (gtk_accel_path "/Compile/Compile" "") +; (gtk_accel_path "/File/Save all" "") +; (gtk_accel_path "/Tactics/Tactic fix" "") +; (gtk_accel_path "/Templates/Template Parameter" "") +; (gtk_accel_path "/Tactics/Tactic assert" "") +; (gtk_accel_path "/Tactics/Tactic do" "") +; (gtk_accel_path "/Tactics/Tactic ring" "") +; (gtk_accel_path "/Export/Pdf" "") +; (gtk_accel_path "/Tactics/Tactic quote" "") +; (gtk_accel_path "/Tactics/Tactic symmetry in" "") +; (gtk_accel_path "/Help/Help" "") +(gtk_accel_path "/Templates/Inductive" "i") +; (gtk_accel_path "/Tactics/Tactic idtac" "") +; (gtk_accel_path "/Templates/Template Syntax" "") +; (gtk_accel_path "/Tactics/Tactic intro -- after" "") +; (gtk_accel_path "/Tactics/Tactic fold -- in" "") +; (gtk_accel_path "/Templates/Template Program Definition" "") +(gtk_accel_path "/Tactics/Wizard" "dollar") +; (gtk_accel_path "/Templates/Template Hint Resolve" "") +; (gtk_accel_path "/Templates/Template Set Extraction Optimize" "") ; (gtk_accel_path "/File/Revert all buffers" "") -; (gtk_accel_path "/Templates/_P.../" "") -; (gtk_accel_path "/t_rivial/" "") -(gtk_accel_path "/Display/Display existential variable instances" "e") -; (gtk_accel_path "/Tactics/_j.../" "") -; (gtk_accel_path "/A_dd LoadPath/" "") -; (gtk_accel_path "/N_otation/" "") -; (gtk_accel_path "/Edit/Preferences" "") -; (gtk_accel_path "/L_oad Verbose/" "") -; (gtk_accel_path "/i_ntro __ after/" "") -; (gtk_accel_path "/D_erive Dependent Inversion/" "") -; (gtk_accel_path "/d_ependent inversion __ with/" "") -; (gtk_accel_path "/P_rogram Theorem/" "") -; (gtk_accel_path "/E_xtraction Language/" "") -; (gtk_accel_path "/Templates/_U.../" "") -(gtk_accel_path "/Display/Display raw matching expressions" "m") -; (gtk_accel_path "/c_asetype/" "") -(gtk_accel_path "/Edit/Find Previous" "b") -; (gtk_accel_path "/S_ave./" "") -; (gtk_accel_path "/p_attern/" "") -; (gtk_accel_path "/M_odule/" "") -; (gtk_accel_path "/D_eclare ML Module/" "") -; (gtk_accel_path "/Templates/_H.../" "") -; (gtk_accel_path "/F_act/" "") -; (gtk_accel_path "/A_dd Field/" "") -; (gtk_accel_path "/R_emove LoadPath/" "") -; (gtk_accel_path "/Templates/_Write State/" "") +; (gtk_accel_path "/Tactics/Tactic subst" "") +; (gtk_accel_path "/Tactics/Tactic autorewrite" "") +; (gtk_accel_path "/Tactics/Tactic pose" "") +; (gtk_accel_path "/Tactics/Tactic simplify--eq" "") +; (gtk_accel_path "/Tactics/Tactic clearbody" "") +; (gtk_accel_path "/Tactics/Tactic eauto" "") +; (gtk_accel_path "/Templates/Template Grammar" "") +; (gtk_accel_path "/Tactics/Tactic exact" "") +; (gtk_accel_path "/Templates/Template Unset Implicit Arguments" "") +; (gtk_accel_path "/Templates/Template Extract Inductive" "") +(gtk_accel_path "/View/Display implicit arguments" "i") +; (gtk_accel_path "/Tactics/Tactic symmetry" "") +; (gtk_accel_path "/Templates/Template Add Printing Let" "") +; (gtk_accel_path "/Help/Help for keyword" "h") +; (gtk_accel_path "/File/Save" "s") ; (gtk_accel_path "/Compile/Make makefile" "") -; (gtk_accel_path "/C_oInductive/" "") -; (gtk_accel_path "/Compile/Compile buffer" "") -; (gtk_accel_path "/l_eft/" "") -; (gtk_accel_path "/a_pply __ with/" "") -(gtk_accel_path "/File/Rehighlight" "l") +; (gtk_accel_path "/Templates/Template Remove LoadPath" "") +(gtk_accel_path "/Navigation/Interrupt" "Break") +(gtk_accel_path "/Navigation/End" "End") +; (gtk_accel_path "/Templates/Template Add Morphism" "") +; (gtk_accel_path "/Tactics/Tactic field" "") +; (gtk_accel_path "/Templates/Template Axiom" "") +; (gtk_accel_path "/Tactics/Tactic solve" "") +; (gtk_accel_path "/Tactics/Tactic casetype" "") +; (gtk_accel_path "/Tactics/Tactic cbv in" "") +; (gtk_accel_path "/Templates/Template Load" "") +; (gtk_accel_path "/Tactics/Tactic fourier" "") +; (gtk_accel_path "/Templates/Template Goal" "") +; (gtk_accel_path "/Tactics/Tactic exists" "") +; (gtk_accel_path "/Tactics/Tactic decompose record" "") +(gtk_accel_path "/Navigation/Go to" "Right") +; (gtk_accel_path "/Templates/Template Remark" "") +; (gtk_accel_path "/Templates/Template Set Undo" "") +; (gtk_accel_path "/Templates/Template Inductive" "") +(gtk_accel_path "/Edit/Preferences" "VoidSymbol") +; (gtk_accel_path "/Export/Html" "") +; (gtk_accel_path "/Templates/Template Extraction Inline" "") +; (gtk_accel_path "/Tactics/Tactic absurd" "") +(gtk_accel_path "/Tactics/intuition" "i") +; (gtk_accel_path "/Tactics/Tactic simple induction" "") +; (gtk_accel_path "/Queries/Queries" "") +; (gtk_accel_path "/Tactics/Tactic rewrite -- in" "") +; (gtk_accel_path "/Templates/Template Hint Rewrite" "") +; (gtk_accel_path "/Templates/Template Add Semi Ring A Aplus Amult Aone Azero Aeq T [ c1 ... cn ]." "") +; (gtk_accel_path "/Navigation/Navigation" "") +; (gtk_accel_path "/Help/Browse Coq Manual" "") +; (gtk_accel_path "/Tactics/Tactic transitivity" "") +; (gtk_accel_path "/Tactics/Tactic auto" "") +; (gtk_accel_path "/Tactics/Tactic dependent inversion -- with" "") +; (gtk_accel_path "/Tactics/Tactic assumption" "") +; (gtk_accel_path "/Templates/Template Notation" "") +; (gtk_accel_path "/Edit/Cut" "x") +; (gtk_accel_path "/Templates/Template Theorem" "") +; (gtk_accel_path "/Edit/Close Find" "Escape") +; (gtk_accel_path "/Tactics/Tactic constructor" "") +; (gtk_accel_path "/Tactics/Tactic elim -- with" "") +; (gtk_accel_path "/Templates/Template Identity Coercion" "") +; (gtk_accel_path "/Queries/Whelp Locate" "") +(gtk_accel_path "/View/Display all low-level contents" "l") +; (gtk_accel_path "/Tactics/Tactic right" "") +; (gtk_accel_path "/Edit/Find Previous" "F3") +; (gtk_accel_path "/Tactics/Tactic cofix" "") +; (gtk_accel_path "/Templates/Template Restore State" "") +; (gtk_accel_path "/Templates/Template Lemma" "") +; (gtk_accel_path "/Tactics/Tactic refine" "") +; (gtk_accel_path "/Templates/Template Section" "") +; (gtk_accel_path "/Tactics/Tactic assert (--:=--)" "") +; (gtk_accel_path "/Templates/Template Unset Printing Wildcard" "") +; (gtk_accel_path "/Tactics/Tactic progress" "") +; (gtk_accel_path "/Templates/Template Add Printing If" "") +; (gtk_accel_path "/Templates/Template Chapter" "") +(gtk_accel_path "/File/Print..." "p") +; (gtk_accel_path "/Templates/Template Record" "") +; (gtk_accel_path "/Tactics/Tactic info" "") +; (gtk_accel_path "/Tactics/Tactic firstorder with" "") +; (gtk_accel_path "/Templates/Template Hint Unfold" "") +; (gtk_accel_path "/Templates/Template Set Silent." "") +; (gtk_accel_path "/Templates/Template Program Theorem" "") +; (gtk_accel_path "/Templates/Template Declare ML Module" "") +; (gtk_accel_path "/Tactics/Tactic lazy in" "") +; (gtk_accel_path "/Tactics/Tactic unfold -- in" "") +; (gtk_accel_path "/Edit/Paste" "v") +; (gtk_accel_path "/Templates/Template Remove Printing If" "") +; (gtk_accel_path "/Tactics/Tactic intuition" "") +; (gtk_accel_path "/Queries/SearchAbout" "F2") +; (gtk_accel_path "/Tactics/Tactic dependent rewrite ->" "") +; (gtk_accel_path "/Templates/Template Module" "") +; (gtk_accel_path "/Templates/Template Unset Extraction AutoInline" "") +(gtk_accel_path "/Templates/Scheme" "s") +; (gtk_accel_path "/Templates/Template V" "") +; (gtk_accel_path "/Templates/Template Variable" "") +; (gtk_accel_path "/Tactics/Tactic decide equality" "") +; (gtk_accel_path "/Tactics/Tactic instantiate (--:=--)" "") +; (gtk_accel_path "/Templates/Template Syntactic Definition" "") +; (gtk_accel_path "/Templates/Template Set Extraction AutoInline" "") +; (gtk_accel_path "/Templates/Template Unset Undo" "") +; (gtk_accel_path "/Tactics/Tactic dependent inversion" "") +; (gtk_accel_path "/Tactics/Tactic setoid--rewrite" "") +; (gtk_accel_path "/Templates/Template Add Field" "") +; (gtk_accel_path "/Templates/Template Require Export" "") +; (gtk_accel_path "/Tactics/Tactic rewrite <-" "") +(gtk_accel_path "/Tactics/omega" "o") +; (gtk_accel_path "/Tactics/Tactic split" "") +; (gtk_accel_path "/File/Quit" "q") +(gtk_accel_path "/View/Display existential variable instances" "e") +(gtk_accel_path "/Navigation/Start" "Home") +; (gtk_accel_path "/Tactics/Tactic dependent rewrite <-" "") +; (gtk_accel_path "/Templates/Template U" "") +; (gtk_accel_path "/Templates/Template Variables" "") +; (gtk_accel_path "/Templates/Template S" "") +; (gtk_accel_path "/Tactics/Tactic move -- after" "") +; (gtk_accel_path "/Templates/Template Unset Silent." "") +; (gtk_accel_path "/Templates/Template Local" "") +; (gtk_accel_path "/Templates/Template T" "") +; (gtk_accel_path "/Tactics/Tactic reflexivity" "") +; (gtk_accel_path "/Templates/Template R" "") +; (gtk_accel_path "/Templates/Template Time" "") +; (gtk_accel_path "/Templates/Template P" "") +; (gtk_accel_path "/Tactics/Tactic decompose" "") +; (gtk_accel_path "/Templates/Template N" "") +; (gtk_accel_path "/Templates/Template Eval" "") +; (gtk_accel_path "/Tactics/Tactic congruence" "") +; (gtk_accel_path "/Templates/Template O" "") +; (gtk_accel_path "/Templates/Template E" "") +; (gtk_accel_path "/Templates/Template I" "") +; (gtk_accel_path "/Templates/Template H" "") +; (gtk_accel_path "/Templates/Template Extraction Language" "") +; (gtk_accel_path "/Templates/Template M" "") +; (gtk_accel_path "/Templates/Template Derive Inversion" "") +; (gtk_accel_path "/Tactics/Tactic double induction" "") +; (gtk_accel_path "/Templates/Template L" "") +; (gtk_accel_path "/Templates/Template Derive Inversion--clear" "") +(gtk_accel_path "/View/Display universe levels" "u") +; (gtk_accel_path "/Templates/Template G" "") +; (gtk_accel_path "/Templates/Template F" "") +; (gtk_accel_path "/Tactics/Tactic dependent inversion--clear -- with" "") +; (gtk_accel_path "/Templates/Template D" "") +; (gtk_accel_path "/Edit/Edit" "") +; (gtk_accel_path "/Tactics/Tactic firstorder" "") +; (gtk_accel_path "/Templates/Template C" "") +(gtk_accel_path "/Tactics/simpl" "s") +; (gtk_accel_path "/Tactics/Tactic replace -- with" "") +; (gtk_accel_path "/Templates/Template A" "") +; (gtk_accel_path "/Templates/Template Remove Printing Record" "") +; (gtk_accel_path "/Templates/Template Qed." "") +; (gtk_accel_path "/Templates/Template Program Fixpoint" "") +(gtk_accel_path "/View/Display coercions" "c") +; (gtk_accel_path "/Tactics/Tactic hnf" "") +; (gtk_accel_path "/Tactics/Tactic injection" "") +; (gtk_accel_path "/Tactics/Tactic rewrite" "") +; (gtk_accel_path "/Templates/Template Opaque" "") +; (gtk_accel_path "/Templates/Template Focus" "") +; (gtk_accel_path "/Templates/Template Ltac" "") +; (gtk_accel_path "/Tactics/Tactic simple destruct" "") +(gtk_accel_path "/View/Display all basic low-level contents" "a") +; (gtk_accel_path "/Tactics/Tactic jp " "") +; (gtk_accel_path "/Templates/Template Test Printing Synth" "") +; (gtk_accel_path "/Tactics/Tactic set" "") +; (gtk_accel_path "/Edit/External editor" "") +; (gtk_accel_path "/View/Show Toolbar" "") +; (gtk_accel_path "/Tactics/Tactic try" "") +; (gtk_accel_path "/Tactics/Tactic discriminate" "") +(gtk_accel_path "/Templates/Fixpoint" "f") +(gtk_accel_path "/Edit/Complete Word" "slash") +(gtk_accel_path "/Navigation/Next" "greater") +; (gtk_accel_path "/Tactics/Tactic elimtype" "") +; (gtk_accel_path "/Templates/Template End" "") +; (gtk_accel_path "/Templates/Template Fixpoint" "") +; (gtk_accel_path "/View/Next tab" "Right") ; (gtk_accel_path "/File/File" "") -; (gtk_accel_path "/D_erive Dependent Inversion__clear/" "") -; (gtk_accel_path "/d_ecompose/" "") -; (gtk_accel_path "/r_ewrite __ in/" "") -(gtk_accel_path "/Display/Display implicit arguments" "i") -; (gtk_accel_path "/e_lim __ using/" "") -; (gtk_accel_path "/a_ssert (__:=__)/" "") -; (gtk_accel_path "/i_nversion __ using/" "") -; (gtk_accel_path "/P_arameter/" "") -; (gtk_accel_path "/H_int Constructors/" "") -; (gtk_accel_path "/j_p /" "") -; (gtk_accel_path "/p_rogress/" "") -; (gtk_accel_path "/Templates/_M.../" "") -; (gtk_accel_path "/e_lim __ with/" "") -; (gtk_accel_path "/f_irst/" "") -; (gtk_accel_path "/l_azy/" "") -; (gtk_accel_path "/i_nversion/" "") -(gtk_accel_path "/Help/Help for keyword" "h") -; (gtk_accel_path "/a_uto/" "") -; (gtk_accel_path "/G_oal/" "") -; (gtk_accel_path "/i_nversion __ using __ in/" "") -(gtk_accel_path "/Tactics/intuition" "i") -; (gtk_accel_path "/r_ed in/" "") -; (gtk_accel_path "/Tactics/_g.../" "") -; (gtk_accel_path "/g_eneralize dependent/" "") -; (gtk_accel_path "/Queries/About" "F5") -; (gtk_accel_path "/r_ight/" "") -(gtk_accel_path "/Tactics/auto" "a") -(gtk_accel_path "/Templates/Fixpoint" "f") -; (gtk_accel_path "/r_eflexivity/" "") -; (gtk_accel_path "/i_nduction/" "") -; (gtk_accel_path "/i_ntuition/" "") -; (gtk_accel_path "/Tactics/_t.../" "") -; (gtk_accel_path "/f_ix/" "") -; (gtk_accel_path "/Export/Pdf" "") -; (gtk_accel_path "/N_ext Obligation/" "") -(gtk_accel_path "/Tactics/auto with *" "asterisk") -; (gtk_accel_path "/R_ecord/" "") -; (gtk_accel_path "/P_roof./" "") -; (gtk_accel_path "/c_ontradiction/" "") -; (gtk_accel_path "/S_et Extraction AutoInline/" "") -; (gtk_accel_path "/e_auto/" "") -; (gtk_accel_path "/d_ecompose record/" "") -; (gtk_accel_path "/f_ield/" "") -; (gtk_accel_path "/E_val/" "") -; (gtk_accel_path "/R_eset Extraction Inline/" "") +; (gtk_accel_path "/Tactics/Tactic setoid--replace" "") +; (gtk_accel_path "/Tactics/Tactic generalize dependent" "") +(gtk_accel_path "/Tactics/trivial" "v") +; (gtk_accel_path "/Tactics/Tactic fix -- with" "") +; (gtk_accel_path "/Tactics/Tactic pose --:=--)" "") +; (gtk_accel_path "/Tactics/Tactic auto with" "") +; (gtk_accel_path "/Templates/Template Add Printing Record" "") +; (gtk_accel_path "/Tactics/Tactic inversion -- in" "") +(gtk_accel_path "/Tactics/eauto" "e") +; (gtk_accel_path "/File/Open" "o") +; (gtk_accel_path "/Tactics/Tactic elim -- using" "") +; (gtk_accel_path "/Templates/Template Hint" "") +; (gtk_accel_path "/Tactics/Tactic tauto" "") +; (gtk_accel_path "/Export/Dvi" "") +; (gtk_accel_path "/Tactics/Tactic simpl -- in" "") +; (gtk_accel_path "/Templates/Template Hint Immediate" "") -- cgit v1.2.3