Moving configuration of coqide.keys to the coqide executable.

4 files changed, 12 insertions, 378 deletions

diff --git a/.gitignore b/.gitignore
index 93b874eae3..587a6191ab 100644
--- a/.gitignore
+++ b/.gitignore
@@ -191,3 +191,5 @@ theories/*/*/*/dune
 /user-contrib/Ltac2/dune
 *.install
 !Makefile.install
+
+ide/coqide.keys
diff --git a/Makefile.ide b/Makefile.ide
index 0a11f83a18..081d15a1a2 100644
--- a/Makefile.ide
+++ b/Makefile.ide
@@ -59,7 +59,7 @@ IDEBINDINGS:=ide/default.bindings
 IDEBINDINGSSRC:=ide/default_bindings_src.ml
 IDEBINDINGSEXE:=ide/default_bindings_src.exe
 
-IDEFILES=$(wildcard ide/*.lang) ide/coq_style.xml ide/coq.png ide/MacOS/default_accel_map $(IDEBINDINGS)
+IDEFILES=$(wildcard ide/*.lang) ide/coq_style.xml ide/coq.png $(IDEBINDINGS)
 
 ## GTK for Coqide MacOS bundle
 
@@ -175,7 +175,6 @@ $(IDEBINDINGSEXE): $(IDEBINDINGSSRC)
 $(IDEBINDINGS): $(IDEBINDINGSEXE)
 	$< $@
 
-
 ####################
 ## Install targets
 ####################
@@ -224,7 +223,6 @@ install-ide-files: #Please update $(COQIDEAPP)/Contents/Resources/ at the same t
 	$(MKDIR) $(FULLDATADIR)
 	$(INSTALLLIB) ide/coq.png ide/*.lang ide/coq_style.xml $(IDEBINDINGS) $(FULLDATADIR)
 	$(MKDIR) $(FULLCONFIGDIR)
-	if [ $(IDEINT) = QUARTZ ] ; then $(INSTALLLIB) ide/mac_default_accel_map $(FULLCONFIGDIR)/coqide.keys ; fi
 
 install-ide-info:
 	$(MKDIR) $(FULLDOCDIR)
@@ -271,7 +269,6 @@ $(COQIDEAPP)/Contents/Resources/immodules: $(COQIDEAPP)/Contents
 
 $(COQIDEAPP)/Contents/Resources/etc: $(COQIDEAPP)/Contents/Resources/lib
 	$(MKDIR) $@/xdg/coq
-	$(INSTALLLIB) ide/MacOS/default_accel_map $@/xdg/coq/coqide.keys
 	$(MKDIR) $@/gtk-3.0
 	{ "$(PIXBUFBIN)/gdk-pixbuf-query-loaders" $@/../loaders/*.so |\
 	 sed -e "s!/.*\(/loaders/.*.so\)!@executable_path/../Resources/\1!"; } \
diff --git a/ide/MacOS/default_accel_map b/ide/MacOS/default_accel_map
deleted file mode 100644
index 4093d2012b..0000000000
--- a/ide/MacOS/default_accel_map
+++ /dev/null
@@ -1,366 +0,0 @@
-; coqide GtkAccelMap rc-file         -*- scheme -*-
-; this file is an automated accelerator map dump
-;
-; (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/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 "<Actions>/Tactics/Tactic inversion" "")
-; (gtk_accel_path "<Actions>/Templates/Template Write State" "")
-; (gtk_accel_path "<Actions>/Export/Export to" "")
-; (gtk_accel_path "<Actions>/Tactics/Tactic inversion--clear" "")
-; (gtk_accel_path "<Actions>/Templates/Template Implicit Arguments" "")
-; (gtk_accel_path "<Actions>/Edit/Copy" "<Primary>c")
-; (gtk_accel_path "<Actions>/Tactics/Tactic inversion -- using" "")
-; (gtk_accel_path "<Actions>/View/Previous tab" "<Shift>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>/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>/Compile/Compile buffer" "")
-; (gtk_accel_path "<Actions>/Queries/About" "F5")
-; (gtk_accel_path "<Actions>/Templates/Template CoInductive" "")
-; (gtk_accel_path "<Actions>/Templates/Template Test Printing Wildcard" "")
-; (gtk_accel_path "<Actions>/Templates/Template Unset Hyps--limit" "")
-; (gtk_accel_path "<Actions>/Templates/Template Transparent" "")
-; (gtk_accel_path "<Actions>/Export/Ps" "")
-; (gtk_accel_path "<Actions>/Tactics/Tactic elim" "")
-; (gtk_accel_path "<Actions>/Templates/Template Extract Constant" "")
-; (gtk_accel_path "<Actions>/Tactics/Tactic assert (--:--)" "")
-; (gtk_accel_path "<Actions>/Templates/Template Add Rec LoadPath" "")
-; (gtk_accel_path "<Actions>/Edit/Redo" "")
-; (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 If" "")
-; (gtk_accel_path "<Actions>/Templates/Template Load Verbose" "")
-; (gtk_accel_path "<Actions>/Templates/Template Reset Extraction Inline" "")
-; (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 "<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 Proof." "")
-; (gtk_accel_path "<Actions>/Compile/Make" "F6")
-; (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 Set Hyps--limit" "")
-; (gtk_accel_path "<Actions>/Templates/Template Global Variable" "")
-; (gtk_accel_path "<Actions>/Templates/Template Remove Printing Constructor" "")
-; (gtk_accel_path "<Actions>/Templates/Template Add Setoid" "")
-; (gtk_accel_path "<Actions>/Edit/Find Next" "F3")
-; (gtk_accel_path "<Actions>/Edit/Find" "<Primary>f")
-; (gtk_accel_path "<Actions>/Templates/Template Add Relation" "")
-; (gtk_accel_path "<Actions>/Queries/Print" "F4")
-; (gtk_accel_path "<Actions>/Templates/Template Obligations Tactic" "")
-; (gtk_accel_path "<Actions>/Tactics/Tactic trivial" "")
-; (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" "<Control>Escape")
-; (gtk_accel_path "<Actions>/Tactics/Tactic cbv" "")
-; (gtk_accel_path "<Actions>/Tactics/Tactic inversion--clear -- in" "")
-; (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>/Navigation/Backward" "<Primary><Control>Up")
-; (gtk_accel_path "<Actions>/Tactics/Tactic p" "")
-(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>/Tactics/Tactic d" "")
-; (gtk_accel_path "<Actions>/Tactics/Tactic u" "")
-; (gtk_accel_path "<Actions>/Templates/Templates" "")
-; (gtk_accel_path "<Actions>/Tactics/Tactic s" "")
-; (gtk_accel_path "<Actions>/Tactics/Tactic lapply" "")
-; (gtk_accel_path "<Actions>/Tactics/Tactic t" "")
-; (gtk_accel_path "<Actions>/Tactics/Tactic r" "")
-; (gtk_accel_path "<Actions>/Edit/Replace" "<Primary>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>/Templates/Template Definition" "")
-; (gtk_accel_path "<Actions>/Tactics/Tactic g" "")
-; (gtk_accel_path "<Actions>/Tactics/Tactic f" "")
-; (gtk_accel_path "<Actions>/Tactics/Tactic e" "")
-; (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/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>/Tactics/Tactic idtac" "")
-; (gtk_accel_path "<Actions>/Templates/Template Syntax" "")
-; (gtk_accel_path "<Actions>/Tactics/Tactic intro -- after" "")
-; (gtk_accel_path "<Actions>/Tactics/Tactic fold -- in" "")
-; (gtk_accel_path "<Actions>/Templates/Template Program Definition" "")
-; (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 "<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 "<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>/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>,")
-; (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/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>/Tactics/Tactic constructor" "")
-; (gtk_accel_path "<Actions>/Tactics/Tactic elim -- with" "")
-; (gtk_accel_path "<Actions>/Templates/Template Identity Coercion" "")
-(gtk_accel_path "<Actions>/View/Display all low-level contents" "<Shift><Control>l")
-; (gtk_accel_path "<Actions>/Tactics/Tactic right" "")
-; (gtk_accel_path "<Actions>/Edit/Find Previous" "<Shift>F3")
-; (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>/Templates/Template Unset Printing Wildcard" "")
-; (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>/Tactics/Tactic setoid--rewrite" "")
-; (gtk_accel_path "<Actions>/Templates/Template Add Field" "")
-; (gtk_accel_path "<Actions>/Templates/Template Require Export" "")
-; (gtk_accel_path "<Actions>/Tactics/Tactic rewrite <-" "")
-; (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/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>/Tactics/Tactic try" "")
-; (gtk_accel_path "<Actions>/Tactics/Tactic discriminate" "")
-(gtk_accel_path "<Actions>/Templates/Fixpoint" "<Shift><Primary>f")
-(gtk_accel_path "<Actions>/Edit/Complete Word" "<Primary>slash")
-(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" "<Shift>Right")
-; (gtk_accel_path "<Actions>/File/File" "")
-; (gtk_accel_path "<Actions>/Tactics/Tactic setoid--replace" "")
-; (gtk_accel_path "<Actions>/Tactics/Tactic generalize dependent" "")
-; (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>/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/preferences.ml b/ide/preferences.ml
index 10d779263b..2cc98e6927 100644
--- a/ide/preferences.ml
+++ b/ide/preferences.ml
@@ -321,17 +321,23 @@ let attach_modifiers (pref : string preference) prefix =
   in
   pref#connect#changed ~callback:cb
 
+let select_arch m m_osx =
+  if Coq_config.arch = "Darwin" then m_osx else m
+
 let modifier_for_navigation =
-  new preference ~name:["modifier_for_navigation"] ~init:"<Control>" ~repr:Repr.(string)
+  new preference ~name:["modifier_for_navigation"]
+    ~init:(select_arch "<Control>" "<Control><Primary>") ~repr:Repr.(string)
 
 let modifier_for_templates =
   new preference ~name:["modifier_for_templates"] ~init:"<Control><Shift>" ~repr:Repr.(string)
 
 let modifier_for_tactics =
-  new preference ~name:["modifier_for_tactics"] ~init:"<Control><Alt>" ~repr:Repr.(string)
+  new preference ~name:["modifier_for_tactics"]
+    ~init:(select_arch "<Control><Alt>" "<Control><Primary>") ~repr:Repr.(string)
 
 let modifier_for_display =
-  new preference ~name:["modifier_for_display"] ~init:"<Alt><Shift>" ~repr:Repr.(string)
+  new preference ~name:["modifier_for_display"]
+    ~init:(select_arch "<Alt><Shift>" "<Primary><Shift>")~repr:Repr.(string)
 
 let modifier_for_queries =
   new preference ~name:["modifier_for_queries"] ~init:"<Control><Shift>" ~repr:Repr.(string)
@@ -684,11 +690,6 @@ let load_pref_file loader warn name =
     try_load_pref_file loader warn old_user_file
   with Not_found ->
   (* Built-in configuration *)
-  try
-    let default_file = get_config_file [Minilib.coqide_default_config_dir ()] name in
-    warn ~delay:5000 ("No " ^ name ^ ", using default configuration file");
-    try_load_pref_file loader warn default_file
-  with Not_found ->
     warn ~delay:5000 ("No " ^ name ^ ", using default internal configuration")
 
 let load_accel_pref ~warn =