Merge PR #8567: More general support for installation of coqide keys

Ack-by: SkySkimmer
Reviewed-by: Zimmi48
Reviewed-by: ejgallego
Reviewed-by: gares
Ack-by: ppedrot

14 files changed, 161 insertions, 445 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/clib/cString.ml b/clib/cString.ml
index 60915efe86..99fb7d2b78 100644
--- a/clib/cString.ml
+++ b/clib/cString.ml
@@ -24,6 +24,7 @@ sig
   val conjugate_verb_to_be : int -> string
   val ordinal : int -> string
   val is_sub : string -> string -> int -> bool
+  val is_prefix : string -> string -> bool
   module Set : Set.S with type elt = t
   module Map : CMap.ExtS with type key = t and module Set := Set
   module List : CList.MonoS with type elt = t
@@ -101,6 +102,9 @@ let is_sub p s off =
     in
     aux 0
 
+let is_prefix p s =
+  is_sub p s 0
+
 let plural n s = if n<>1 then s^"s" else s
 
 let conjugate_verb_to_be n = if n<>1 then "are" else "is"
diff --git a/clib/cString.mli b/clib/cString.mli
index 8a4fe62a1c..d02be2d15f 100644
--- a/clib/cString.mli
+++ b/clib/cString.mli
@@ -51,6 +51,9 @@ sig
   val is_sub : string -> string -> int -> bool
   (** [is_sub p s off] tests whether [s] contains [p] at offset [off]. *)
 
+  val is_prefix : string -> string -> bool
+  (** [is_prefix p s] tests whether [p] is a prefix of [s]. *)
+
   (** {6 Generic operations} **)
 
   module Set : Set.S with type elt = t
diff --git a/configure.ml b/configure.ml
index cef4faaf1a..d7370b28c1 100644
--- a/configure.ml
+++ b/configure.ml
@@ -1200,8 +1200,8 @@ let write_macos_metadata exec =
   let () = close_out o in
   Unix.chmod f 0o444
 
-let () = if arch = "Darwin" then
-List.iter write_macos_metadata distributed_exec
+let () =
+  if arch = "Darwin" then List.iter write_macos_metadata distributed_exec
 
 let write_configpy f =
   safe_remove f;
diff --git a/doc/sphinx/practical-tools/coqide.rst b/doc/sphinx/practical-tools/coqide.rst
index 7d6171285e..b1f392c337 100644
--- a/doc/sphinx/practical-tools/coqide.rst
+++ b/doc/sphinx/practical-tools/coqide.rst
@@ -179,10 +179,13 @@ compilation, printing, web browsing. In the browser command, you may
 use `%s` to denote the URL to open, for example:
 `firefox -remote "OpenURL(%s)"`.
 
-Notice that these settings are saved in the file `.coqiderc` of your
-home directory.
+Notice that these settings are saved in the file ``coqiderc`` in the
+``coq`` subdirectory of the user configuration directory which
+is the value of ``$XDG_CONFIG_HOME`` if this environment variable is
+set and which otherwise is ``$HOME/.config/``.
 
-A Gtk2 accelerator keymap is saved under the name `.coqide.keys`. It
+A GTK+ accelerator keymap is saved under the name ``coqide.keys`` in
+the same ``coq`` subdirectory of the user configuration directory. It
 is not recommended to edit this file manually: to modify a given menu
 shortcut, go to the corresponding menu item without releasing the
 mouse button, press the key you want for the new shortcut, and release
@@ -259,8 +262,9 @@ Adding custom bindings
 ~~~~~~~~~~~~~~~~~~~~~~
 
 To extend the default set of bindings, create a file named ``coqide.bindings``
-and place it in the same folder as ``coqide.keys``. On Linux, this would be
-the folder ``~/.config/coq``. The file `coqide.bindings` should contain one
+and place it in the same folder as ``coqide.keys``. This would be
+the folder ``$XDG_CONFIG_HOME/coq``, defaulting to ``~/.config/coq``
+if ``XDG_CONFIG_HOME`` is unset. The file `coqide.bindings` should contain one
 binding per line, in the form ``\key value``, followed by an optional priority
 integer. (The key and value should not contain any space character.)
 
diff --git a/ide/MacOS/default_accel_map b/ide/MacOS/default_accel_map
deleted file mode 100644
index 6bcf3b438f..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>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/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/coqide.ml b/ide/coqide.ml
index 9cdfd0dc21..70fa61b208 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -1016,7 +1016,7 @@ let build_ui () =
 
   menu edit_menu [
     item "Edit" ~label:"_Edit";
-    item "Undo" ~accel:"<Ctrl>u" ~stock:`UNDO
+    item "Undo" ~accel:"<Primary>u" ~stock:`UNDO
       ~callback:(cb_on_current_term (fun t -> t.script#undo ()));
     item "Redo" ~stock:`REDO
       ~callback:(cb_on_current_term (fun t -> t.script#redo ()));
@@ -1035,7 +1035,7 @@ let build_ui () =
       ~callback:(cb_on_current_term (fun t -> t.finder#find_backward ()));
     item "External editor" ~label:"External editor" ~stock:`EDIT
       ~callback:(External.editor ~parent:w);
-    item "Preferences" ~accel:"<Ctrl>comma" ~stock:`PREFERENCES
+    item "Preferences" ~accel:"<Primary>comma" ~stock:`PREFERENCES
       ~callback:(fun _ ->
         begin
 	  try Preferences.configure ~apply:refresh_notebook_pos w
@@ -1053,19 +1053,19 @@ let build_ui () =
     item "Next tab" ~label:"_Next tab" ~accel:"<Alt>Right"
       ~stock:`GO_FORWARD
       ~callback:(fun _ -> notebook#next_page ());
-    item "Zoom in" ~label:"_Zoom in" ~accel:("<Control>plus")
+    item "Zoom in" ~label:"_Zoom in" ~accel:("<Primary>plus")
         ~stock:`ZOOM_IN ~callback:(fun _ ->
           let ft = Pango.Font.from_string text_font#get in
           Pango.Font.set_size ft (Pango.Font.get_size ft + Pango.scale);
           text_font#set (Pango.Font.to_string ft);
           save_pref ());
-    item "Zoom out" ~label:"_Zoom out" ~accel:("<Control>minus")
+    item "Zoom out" ~label:"_Zoom out" ~accel:("<Primary>minus")
         ~stock:`ZOOM_OUT ~callback:(fun _ ->
           let ft = Pango.Font.from_string text_font#get in
           Pango.Font.set_size ft (Pango.Font.get_size ft - Pango.scale);
           text_font#set (Pango.Font.to_string ft);
           save_pref ());
-    item "Zoom fit" ~label:"_Zoom fit" ~accel:("<Control>0")
+    item "Zoom fit" ~label:"_Zoom fit" ~accel:("<Primary>0")
         ~stock:`ZOOM_FIT ~callback:(cb_on_current_term MiscMenu.zoom_fit);
     toggle_item "Show Toolbar" ~label:"Show _Toolbar"
       ~active:(show_toolbar#get)
@@ -1247,7 +1247,6 @@ let build_ui () =
   let () = refresh_notebook_pos () in
   let lower_hbox = GPack.hbox ~homogeneous:false ~packing:vbox#pack () in
   let () = lower_hbox#pack ~expand:true status#coerce in
-  let () = push_info ("Ready"^ if microPG#get then ", [μPG]" else "")  in
 
   (* Location display *)
   let l = GMisc.label
@@ -1372,7 +1371,7 @@ let read_coqide_args argv =
     |"-coqtop-flags" :: flags :: args->
       Coq.ideslave_coqtop_flags := Some flags;
       filter_coqtop coqtop project_files bindings_files out args
-    |arg::args when out = [] && Minilib.is_prefix_of "-psn_" arg ->
+    |arg::args when out = [] && CString.is_prefix "-psn_" arg ->
       (* argument added by MacOS during .app launch *)
       filter_coqtop coqtop project_files bindings_files out args
     |arg::args -> filter_coqtop coqtop project_files bindings_files (arg::out) args
diff --git a/ide/coqide_main.ml b/ide/coqide_main.ml
index f2ce2e8bd9..1e04d269f6 100644
--- a/ide/coqide_main.ml
+++ b/ide/coqide_main.ml
@@ -49,11 +49,10 @@ let catch_gtk_messages () =
 let () = catch_gtk_messages ()
 
 let load_prefs () =
-  try Preferences.load_pref ()
-  with e -> Ideutils.flash_info
-    ("Could not load preferences ("^Printexc.to_string e^").")
+  Preferences.load_pref ~warn:(fun ~delay -> Ideutils.flash_info ~delay)
 
 let () =
+  Ideutils.push_info ("Ready"^ if Preferences.microPG#get then ", [μPG]" else "");
   load_prefs ();
   let argl = List.tl (Array.to_list Sys.argv) in
   let argl = Coqide.read_coqide_args argl in
diff --git a/ide/ideutils.ml b/ide/ideutils.ml
index 246254c6a5..4b156065f3 100644
--- a/ide/ideutils.ml
+++ b/ide/ideutils.ml
@@ -34,9 +34,38 @@ let push_info,pop_info,clear_info =
   (fun () -> decr size; status_context#pop ()),
   (fun () -> for _i = 1 to !size do status_context#pop () done; size := 0)
 
+type 'a mlist = Nil | Cons of { hd : 'a ; mutable tl : 'a mlist }
+
+let enqueue a x =
+  let rec aux x = match x with
+    | Nil -> assert false
+    | Cons p ->
+      match p.tl with
+      | Nil -> p.tl <- Cons { hd = a ; tl = Nil }
+      | _ -> aux p.tl in
+  match !x with
+  | Nil -> x := Cons { hd = a ; tl = Nil }
+  | _ -> aux !x
+
+let pop = function
+  | Cons p -> p.tl
+  | Nil -> assert false
+
 let flash_info =
+  let queue = ref Nil in
   let flash_context = status#new_context ~name:"Flash" in
-    (fun ?(delay=5000) s -> flash_context#flash ~delay s)
+  let rec process () = match !queue with
+    | Cons { hd = (delay,text) } ->
+       let msg = flash_context#push text in
+       ignore (Glib.Timeout.add ~ms:delay ~callback:(fun () ->
+                   flash_context#remove msg;
+                   queue := pop !queue;
+                   process (); false))
+    | Nil -> () in
+  fun ?(delay=5000) text ->
+    let processing = !queue <> Nil in
+    enqueue (delay,text) queue;
+    if not processing then process ()
 
 (* Note: Setting the same attribute with two separate tags appears to use
 the first value applied and not the second.  I saw this trying to set the background
diff --git a/ide/minilib.ml b/ide/minilib.ml
index 09a7112098..926ad27abc 100644
--- a/ide/minilib.ml
+++ b/ide/minilib.ml
@@ -58,17 +58,13 @@ let coqide_data_dirs () =
   :: List.map coqify (Glib.get_system_data_dirs ())
   @ [Envars.datadir ()]
 
-let coqide_config_dirs () =
-  coqide_config_home ()
-  :: List.map coqify (Glib.get_system_config_dirs ())
-  @ [Envars.configdir ()]
+let coqide_system_config_dirs () =
+  List.map coqify (Glib.get_system_config_dirs ())
 
-let is_prefix_of pre s =
-  let i = ref 0 in
-  let () = while (!i < (String.length pre)
-        && !i < (String.length s)
-	     && pre.[!i] = s.[!i]) do
-	          incr i
-		     done
-  in !i = String.length pre
+let coqide_default_config_dir () =
+  Envars.configdir ()
 
+let coqide_config_dirs () =
+  coqide_config_home () ::
+  coqide_system_config_dirs () @
+  [coqide_default_config_dir ()]
diff --git a/ide/minilib.mli b/ide/minilib.mli
index c5849cc2c9..a9d26ee7d2 100644
--- a/ide/minilib.mli
+++ b/ide/minilib.mli
@@ -27,7 +27,19 @@ val debug : bool ref
 val log_pp : ?level:level -> Pp.t -> unit
 val log    : ?level:level -> string        -> unit
 
+(* The directory where user config files are conventionally *)
+(* installed on the current platform (as given by Glib) *)
 val coqide_config_home : unit -> string
+
+(* The directories where system-wide config files are conventionally *)
+(* installed on the current platform (as given by Glib) *)
+val coqide_system_config_dirs : unit -> string list
+
+(* The directory where default config files are installed at installation time *)
+val coqide_default_config_dir : unit -> string
+
+(* The ordered list of directories where a config file is searched by default *)
 val coqide_config_dirs : unit -> string list
+
+(* The ordered list of directories where a data file is searched by default *)
 val coqide_data_dirs : unit -> string list
-val is_prefix_of : string -> string -> bool
diff --git a/ide/preferences.ml b/ide/preferences.ml
index bf9fe8922a..7b667027fc 100644
--- a/ide/preferences.ml
+++ b/ide/preferences.ml
@@ -10,8 +10,6 @@
 
 open Configwin
 
-let pref_file = Filename.concat (Minilib.coqide_config_home ()) "coqiderc"
-let accel_file = Filename.concat (Minilib.coqide_config_home ()) "coqide.keys"
 let lang_manager = GSourceView3.source_language_manager ~default:true
 let () = lang_manager#set_search_path
   ((Minilib.coqide_data_dirs ())@lang_manager#search_path)
@@ -235,22 +233,13 @@ end
 
 end
 
-let get_config_file name =
+let get_config_file dirs name =
   let find_config dir = Sys.file_exists (Filename.concat dir name) in
-  let config_dir = List.find find_config (Minilib.coqide_config_dirs ()) in
+  let config_dir = List.find find_config dirs in
   Filename.concat config_dir name
 
-(* Small hack to handle v8.3 to v8.4 change in configuration file *)
-let loaded_pref_file =
-  try get_config_file "coqiderc"
-  with Not_found -> Filename.concat (Option.default "" (Glib.get_home_dir ())) ".coqiderc"
-
-let loaded_accel_file =
-  try get_config_file "coqide.keys"
-  with Not_found -> Filename.concat (Option.default "" (Glib.get_home_dir ())) ".coqide.keys"
-
 let get_unicode_bindings_local_file () =
-  try Some (get_config_file "coqide.bindings")
+  try Some (get_config_file [Minilib.coqide_config_home ()] "coqide.bindings")
   with Not_found -> None
 
 let get_unicode_bindings_default_file () =
@@ -332,26 +321,36 @@ 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)
 
-let _ = attach_modifiers modifier_for_navigation "<Actions>/Navigation/"
-let _ = attach_modifiers modifier_for_templates "<Actions>/Templates/"
-let _ = attach_modifiers modifier_for_tactics "<Actions>/Tactics/"
-let _ = attach_modifiers modifier_for_display "<Actions>/View/"
-let _ = attach_modifiers modifier_for_queries "<Actions>/Queries/"
+let attach_modifiers_callback () =
+  (* Tell to propagate changes done in preference menu to accel map *)
+  (* To be done after the preferences are loaded *)
+  let _ = attach_modifiers modifier_for_navigation "<Actions>/Navigation/" in
+  let _ = attach_modifiers modifier_for_templates "<Actions>/Templates/" in
+  let _ = attach_modifiers modifier_for_tactics "<Actions>/Tactics/" in
+  let _ = attach_modifiers modifier_for_display "<Actions>/View/" in
+  let _ = attach_modifiers modifier_for_queries "<Actions>/Queries/" in
+  ()
 
 let modifiers_valid =
   new preference ~name:["modifiers_valid"] ~init:"<Alt><Control><Shift>" ~repr:Repr.(string)
@@ -380,9 +379,6 @@ let text_font =
 let show_toolbar =
   new preference ~name:["show_toolbar"] ~init:true ~repr:Repr.(bool)
 
-let contextual_menus_on_goal =
-  new preference ~name:["contextual_menus_on_goal"] ~init:true ~repr:Repr.(bool)
-
 let window_width =
   new preference ~name:["window_width"] ~init:800 ~repr:Repr.(int)
 
@@ -644,29 +640,73 @@ let tag_button () =
   let box = GPack.hbox () in
   new tag_button (Gobject.unsafe_cast box#as_widget)
 
-let save_pref () =
+(** Loading/saving preferences *)
+
+let pref_file = Filename.concat (Minilib.coqide_config_home ()) "coqiderc"
+let accel_file = Filename.concat (Minilib.coqide_config_home ()) "coqide.keys"
+
+let save_accel_pref () =
+  if not (Sys.file_exists (Minilib.coqide_config_home ()))
+  then Unix.mkdir (Minilib.coqide_config_home ()) 0o700;
+  GtkData.AccelMap.save accel_file
+
+let save_rc_pref () =
   if not (Sys.file_exists (Minilib.coqide_config_home ()))
   then Unix.mkdir (Minilib.coqide_config_home ()) 0o700;
-  let () = try GtkData.AccelMap.save accel_file with _ -> () in
   let add = Util.String.Map.add in
   let fold key obj accu = add key (obj.get ()) accu in
   let prefs = Util.String.Map.fold fold !preferences Util.String.Map.empty in
   let prefs = Util.String.Map.fold Util.String.Map.add !unknown_preferences prefs in
   Config_lexer.print_file pref_file prefs
 
-let load_pref () =
-  (* Load main preference file *)
-  let () =
-    let m = Config_lexer.load_file loaded_pref_file in
+let save_pref () =
+  save_accel_pref ();
+  save_rc_pref ()
+
+let try_load_pref_file loader warn file =
+  try
+    loader file
+  with
+    e -> warn ~delay:5000 ("Could not load " ^ file ^ " ("^Printexc.to_string e^")")
+
+let load_pref_file loader warn name =
+  try
+    let user_file = get_config_file [Minilib.coqide_config_home ()] name in
+    warn ~delay:2000 ("Loading " ^ user_file);
+    try_load_pref_file loader warn user_file
+  with Not_found ->
+  try
+    let system_wide_file = get_config_file (Minilib.coqide_system_config_dirs ()) name in
+    warn ~delay:5000 ("No user " ^ name ^ ", using system wide configuration");
+    try_load_pref_file loader warn system_wide_file
+  with Not_found ->
+  (* Compatibility with oldest versions of CoqIDE (<= 8.4) *)
+  try
+    let old_user_file = get_config_file [Option.default "" (Glib.get_home_dir ())] ("."^name) in
+    warn ~delay:5000 ("No " ^ name ^ ", trying to recover from an older version of CoqIDE");
+    try_load_pref_file loader warn old_user_file
+  with Not_found ->
+  (* Built-in configuration *)
+    warn ~delay:5000 ("No " ^ name ^ ", using default internal configuration")
+
+let load_accel_pref ~warn =
+  load_pref_file GtkData.AccelMap.load warn "coqide.keys"
+
+let load_rc_pref ~warn =
+  let loader file =
+    let m = Config_lexer.load_file file in
     let iter name v =
       if Util.String.Map.mem name !preferences then
         try (Util.String.Map.find name !preferences).set v with _ -> ()
       else unknown_preferences := Util.String.Map.add name v !unknown_preferences
     in
     Util.String.Map.iter iter m in
-  (* Load file for bindings *)
-  let () = try GtkData.AccelMap.load loaded_accel_file with _ -> () in
-  ()
+  load_pref_file loader warn "coqiderc";
+  attach_modifiers_callback ()
+
+let load_pref ~warn =
+  load_rc_pref ~warn;
+  load_accel_pref ~warn
 
 let pstring name p = string ~f:p#set name p#get
 let pbool name p = bool ~f:p#set name p#get
@@ -893,19 +933,19 @@ let configure ?(apply=(fun () -> ())) parent =
   in
   let project_file_name = pstring "Default name for project file" project_file_name in
   let modifier_for_tactics =
-    pmodifiers "Modifiers for Tactics Menu" modifier_for_tactics
+    pmodifiers "Global change of modifiers for Tactics Menu" modifier_for_tactics
   in
   let modifier_for_templates =
-    pmodifiers "Modifiers for Templates Menu" modifier_for_templates
+    pmodifiers "Global change of modifiers for Templates Menu" modifier_for_templates
   in
   let modifier_for_navigation =
-    pmodifiers "Modifiers for Navigation Menu" modifier_for_navigation
+    pmodifiers "Global change of modifiers for Navigation Menu" modifier_for_navigation
   in
   let modifier_for_display =
-    pmodifiers "Modifiers for View Menu" modifier_for_display
+    pmodifiers "Global change of modifiers for View Menu" modifier_for_display
   in
   let modifier_for_queries =
-    pmodifiers "Modifiers for Queries Menu" modifier_for_queries
+    pmodifiers "Global change of modifiers for Queries Menu" modifier_for_queries
   in
   let modifiers_valid =
     pmodifiers ~all:true "Allowed modifiers" modifiers_valid
@@ -939,9 +979,7 @@ let configure ?(apply=(fun () -> ())) parent =
       cmd_browse#get
   in
 
-  let contextual_menus_on_goal = pbool "Contextual menus on goal" contextual_menus_on_goal in
-
-  let misc = [contextual_menus_on_goal;stop_before;reset_on_tab_switch;
+  let misc = [stop_before;reset_on_tab_switch;
               vertical_tabs;opposite_tabs] in
 
 (*
diff --git a/ide/preferences.mli b/ide/preferences.mli
index 490756d4f2..4b04326cec 100644
--- a/ide/preferences.mli
+++ b/ide/preferences.mli
@@ -79,7 +79,6 @@ val cmd_browse : string preference
 val cmd_editor : string preference
 val text_font : string preference
 val show_toolbar : bool preference
-val contextual_menus_on_goal : bool preference
 val window_width : int preference
 val window_height : int preference
 val auto_complete : bool preference
@@ -107,7 +106,7 @@ val user_queries : (string * string) list preference
 val diffs : string preference
 
 val save_pref : unit -> unit
-val load_pref : unit -> unit
+val load_pref : warn:(delay:int -> string -> unit) -> unit
 
 val configure : ?apply:(unit -> unit) -> GWindow.window -> unit