Imported Upstream version 8.5~beta1+dfsg

5 files changed, 482 insertions, 0 deletions

diff --git a/ide/MacOS/Info.plist.template b/ide/MacOS/Info.plist.template
new file mode 100644
index 00000000..fd80c839
--- /dev/null
+++ b/ide/MacOS/Info.plist.template
@@ -0,0 +1,89 @@
+<?xml version="1.0" encoding="UTF-8"?>
+<!DOCTYPE plist PUBLIC "-//Apple//DTD PLIST 1.0//EN" "http://www.apple.com/DTDs/PropertyList-1.0.dtd">
+<plist version="1.0">
+<dict>
+	<key>CFBundleDocumentTypes</key>
+	<array>
+		<dict>
+			<key>CFBundleTypeExtensions</key>
+			<array>
+				<string>*</string>
+			</array>
+			<key>CFBundleTypeName</key>
+			<string>NSStringPboardType</string>
+			<key>CFBundleTypeOSTypes</key>
+			<array>
+				<string>****</string>
+			</array>
+			<key>CFBundleTypeRole</key>
+			<string>Editor</string>
+		</dict>
+		<dict>
+			<key>CFBundleTypeIconFile</key>
+			<string>coqfile.icns</string>
+			<key>CFBundleTypeName</key>
+			<string>Coq file</string>
+			<key>CFBundleTypeRole</key>
+			<string>Editor</string>
+			<key>CFBundleTypeMIMETypes</key>
+			<array>
+				<string>text/plain</string>
+			</array>
+			<key>CFBundleTypeExtensions</key>
+			<array>
+				<string>v</string>
+			</array>
+			<key>LSHandlerRank</key>
+			<string>Owner</string>
+		</dict>
+		<dict>
+			<key>CFBundleTypeName</key>
+			<string>All</string>
+			<key>CFBundleTypeRole</key>
+			<string>Editor</string>
+			<key>CFBundleTypeMIMETypes</key>
+			<array>
+				<string>text/plain</string>
+			</array>
+			<key>LSHandlerRank</key>
+			<string>Default</string>
+			<key>CFBundleTypeExtensions</key>
+			<array>
+				<string>*</string>
+			</array>
+		</dict>
+	</array>
+	<key>CFBundleIconFile</key>
+	<string>coqide.icns</string>
+	<key>CFBundleVersion</key>
+	<string>390</string>
+	<key>CFBundleName</key>
+	<string>CoqIDE</string>
+	<key>CFBundleShortVersionString</key>
+	<string>VERSION</string>
+	<key>CFBundleDisplayName</key>
+	<string>Coq Proof Assistant vVERSION</string>
+	<key>CFBundleGetInfoString</key>
+	<string>Coq_vVERSION</string>
+	<key>NSHumanReadableCopyright</key>
+	<string>Copyright 1999-2014, The Coq Development Team INRIA - CNRS - LIX - LRI - PPS</string>
+	<key>CFBundleHelpBookFolder</key>
+	<string>share/doc/coq/html/</string>
+	<key>CFAppleHelpAnchor</key>
+	<string>index</string>
+	<key>CFBundleExecutable</key>
+	<string>coqide</string>
+	<key>CFBundlePackageType</key>
+	<string>APPL</string>
+	<key>CFBundleInfoDictionaryVersion</key>
+	<string>6.0</string>
+	<key>CFBundleIdentifier</key>
+	<string>fr.inria.coq.coqide</string>
+	<key>LSApplicationCategoryType</key>
+	<string>public.app-category.developer-tools</string>
+	<key>CFBundleDevelopmentRegion</key>
+	<string>English</string>
+	<key>NSPrincipalClass</key>
+	<string>NSApplication</string>
+</dict>
+</plist>
diff --git a/ide/MacOS/coqfile.icns b/ide/MacOS/coqfile.icns
new file mode 100644
index 00000000..107e7043
--- /dev/null
+++ b/ide/MacOS/coqfile.icns
diff --git a/ide/MacOS/coqide.icns b/ide/MacOS/coqide.icns
new file mode 100644
index 00000000..92bdfe77
--- /dev/null
+++ b/ide/MacOS/coqide.icns
diff --git a/ide/MacOS/default_accel_map b/ide/MacOS/default_accel_map
new file mode 100644
index 00000000..6f474eb1
--- /dev/null
+++ b/ide/MacOS/default_accel_map
@@ -0,0 +1,378 @@
+; 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/auto" "<Primary><Control>a")
+; (gtk_accel_path "<Actions>/Tactics/Tactic fold" "")
+; (gtk_accel_path "<Actions>/Help/About Coq" "")
+; (gtk_accel_path "<Actions>/Templates/Template Add Ring A Aplus Amult Aone Azero Ainv Aeq T [ c1 ... cn ]. " "")
+; (gtk_accel_path "<Actions>/Templates/Template Hypothesis" "")
+; (gtk_accel_path "<Actions>/Tactics/Tactic repeat" "")
+; (gtk_accel_path "<Actions>/Templates/Template Unset Extraction Optimize" "")
+; (gtk_accel_path "<Actions>/Templates/Template Add Printing Constructor" "")
+; (gtk_accel_path "<Actions>/Windows/Detach View" "")
+; (gtk_accel_path "<Actions>/Tactics/Tactic inversion" "")
+; (gtk_accel_path "<Actions>/Templates/Template Write State" "")
+; (gtk_accel_path "<Actions>/Export/Export to" "")
+(gtk_accel_path "<Actions>/Tactics/auto with *" "<Primary><Control>asterisk")
+; (gtk_accel_path "<Actions>/Tactics/Tactic inversion--clear" "")
+; (gtk_accel_path "<Actions>/Templates/Template Implicit Arguments" "")
+; (gtk_accel_path "<Actions>/Edit/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>/Tactics/eauto with *" "<Primary><Control>ampersand")
+; (gtk_accel_path "<Actions>/Templates/Template Infix" "")
+; (gtk_accel_path "<Actions>/Tactics/Tactic functional induction" "")
+; (gtk_accel_path "<Actions>/Tactics/Tactic clear" "")
+; (gtk_accel_path "<Actions>/Templates/Template End Silent." "")
+; (gtk_accel_path "<Actions>/Tactics/Tactic intros" "")
+; (gtk_accel_path "<Actions>/Tactics/Tactic constructor -- with" "")
+; (gtk_accel_path "<Actions>/Tactics/Tactic destruct" "")
+; (gtk_accel_path "<Actions>/Tactics/Tactic intro after" "")
+; (gtk_accel_path "<Actions>/Tactics/Tactic abstract" "")
+; (gtk_accel_path "<Actions>/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/Try Tactics" "")
+; (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>/Tactics/Wizard" "<Primary><Control>dollar")
+; (gtk_accel_path "<Actions>/Templates/Template Hint Resolve" "")
+; (gtk_accel_path "<Actions>/Templates/Template Set Extraction Optimize" "")
+; (gtk_accel_path "<Actions>/File/Revert all buffers" "")
+; (gtk_accel_path "<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>/Tactics/Tactic fourier" "")
+; (gtk_accel_path "<Actions>/Templates/Template Goal" "")
+; (gtk_accel_path "<Actions>/Tactics/Tactic exists" "")
+; (gtk_accel_path "<Actions>/Tactics/Tactic decompose record" "")
+(gtk_accel_path "<Actions>/Navigation/Go to" "<Primary><Control>Right")
+; (gtk_accel_path "<Actions>/Templates/Template Remark" "")
+; (gtk_accel_path "<Actions>/Templates/Template Set Undo" "")
+; (gtk_accel_path "<Actions>/Templates/Template Inductive" "")
+(gtk_accel_path "<Actions>/Edit/Preferences" "<Primary>VoidSymbol")
+; (gtk_accel_path "<Actions>/Export/Html" "")
+; (gtk_accel_path "<Actions>/Templates/Template Extraction Inline" "")
+; (gtk_accel_path "<Actions>/Tactics/Tactic absurd" "")
+(gtk_accel_path "<Actions>/Tactics/intuition" "<Primary><Control>i")
+; (gtk_accel_path "<Actions>/Tactics/Tactic simple induction" "")
+; (gtk_accel_path "<Actions>/Queries/Queries" "")
+; (gtk_accel_path "<Actions>/Tactics/Tactic rewrite -- in" "")
+; (gtk_accel_path "<Actions>/Templates/Template Hint Rewrite" "")
+; (gtk_accel_path "<Actions>/Templates/Template Add Semi Ring A Aplus Amult Aone Azero Aeq T [ c1 ... cn ]." "")
+; (gtk_accel_path "<Actions>/Navigation/Navigation" "")
+; (gtk_accel_path "<Actions>/Help/Browse Coq Manual" "")
+; (gtk_accel_path "<Actions>/Tactics/Tactic transitivity" "")
+; (gtk_accel_path "<Actions>/Tactics/Tactic auto" "")
+; (gtk_accel_path "<Actions>/Tactics/Tactic dependent inversion -- with" "")
+; (gtk_accel_path "<Actions>/Tactics/Tactic assumption" "")
+; (gtk_accel_path "<Actions>/Templates/Template Notation" "")
+; (gtk_accel_path "<Actions>/Edit/Cut" "<Primary>x")
+; (gtk_accel_path "<Actions>/Templates/Template Theorem" "")
+; (gtk_accel_path "<Actions>/Tactics/Tactic constructor" "")
+; (gtk_accel_path "<Actions>/Tactics/Tactic elim -- with" "")
+; (gtk_accel_path "<Actions>/Templates/Template Identity Coercion" "")
+; (gtk_accel_path "<Actions>/Queries/Whelp Locate" "")
+(gtk_accel_path "<Actions>/View/Display all low-level contents" "<Shift><Control>l")
+; (gtk_accel_path "<Actions>/Tactics/Tactic right" "")
+; (gtk_accel_path "<Actions>/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/omega" "<Primary><Control>o")
+; (gtk_accel_path "<Actions>/Tactics/Tactic split" "")
+; (gtk_accel_path "<Actions>/File/Quit" "<Primary>q")
+(gtk_accel_path "<Actions>/View/Display existential variable instances" "<Shift><Control>e")
+(gtk_accel_path "<Actions>/Navigation/Start" "<Primary><Control>Home")
+; (gtk_accel_path "<Actions>/Tactics/Tactic dependent rewrite <-" "")
+; (gtk_accel_path "<Actions>/Templates/Template U" "")
+; (gtk_accel_path "<Actions>/Templates/Template Variables" "")
+; (gtk_accel_path "<Actions>/Templates/Template S" "")
+; (gtk_accel_path "<Actions>/Tactics/Tactic move -- after" "")
+; (gtk_accel_path "<Actions>/Templates/Template Unset Silent." "")
+; (gtk_accel_path "<Actions>/Templates/Template Local" "")
+; (gtk_accel_path "<Actions>/Templates/Template T" "")
+; (gtk_accel_path "<Actions>/Tactics/Tactic reflexivity" "")
+; (gtk_accel_path "<Actions>/Templates/Template R" "")
+; (gtk_accel_path "<Actions>/Templates/Template Time" "")
+; (gtk_accel_path "<Actions>/Templates/Template P" "")
+; (gtk_accel_path "<Actions>/Tactics/Tactic decompose" "")
+; (gtk_accel_path "<Actions>/Templates/Template N" "")
+; (gtk_accel_path "<Actions>/Templates/Template Eval" "")
+; (gtk_accel_path "<Actions>/Tactics/Tactic congruence" "")
+; (gtk_accel_path "<Actions>/Templates/Template O" "")
+; (gtk_accel_path "<Actions>/Templates/Template E" "")
+; (gtk_accel_path "<Actions>/Templates/Template I" "")
+; (gtk_accel_path "<Actions>/Templates/Template H" "")
+; (gtk_accel_path "<Actions>/Templates/Template Extraction Language" "")
+; (gtk_accel_path "<Actions>/Templates/Template M" "")
+; (gtk_accel_path "<Actions>/Templates/Template Derive Inversion" "")
+; (gtk_accel_path "<Actions>/Tactics/Tactic double induction" "")
+; (gtk_accel_path "<Actions>/Templates/Template L" "")
+; (gtk_accel_path "<Actions>/Templates/Template Derive Inversion--clear" "")
+(gtk_accel_path "<Actions>/View/Display universe levels" "<Shift><Control>u")
+; (gtk_accel_path "<Actions>/Templates/Template G" "")
+; (gtk_accel_path "<Actions>/Templates/Template F" "")
+; (gtk_accel_path "<Actions>/Tactics/Tactic dependent inversion--clear -- with" "")
+; (gtk_accel_path "<Actions>/Templates/Template D" "")
+; (gtk_accel_path "<Actions>/Edit/Edit" "")
+; (gtk_accel_path "<Actions>/Tactics/Tactic firstorder" "")
+; (gtk_accel_path "<Actions>/Templates/Template C" "")
+(gtk_accel_path "<Actions>/Tactics/simpl" "<Primary><Control>s")
+; (gtk_accel_path "<Actions>/Tactics/Tactic replace -- with" "")
+; (gtk_accel_path "<Actions>/Templates/Template A" "")
+; (gtk_accel_path "<Actions>/Templates/Template Remove Printing Record" "")
+; (gtk_accel_path "<Actions>/Templates/Template Qed." "")
+; (gtk_accel_path "<Actions>/Templates/Template Program Fixpoint" "")
+(gtk_accel_path "<Actions>/View/Display coercions" "<Shift><Control>c")
+; (gtk_accel_path "<Actions>/Tactics/Tactic hnf" "")
+; (gtk_accel_path "<Actions>/Tactics/Tactic injection" "")
+; (gtk_accel_path "<Actions>/Tactics/Tactic rewrite" "")
+; (gtk_accel_path "<Actions>/Templates/Template Opaque" "")
+; (gtk_accel_path "<Actions>/Templates/Template Focus" "")
+; (gtk_accel_path "<Actions>/Templates/Template Ltac" "")
+; (gtk_accel_path "<Actions>/Tactics/Tactic simple destruct" "")
+(gtk_accel_path "<Actions>/View/Display all basic low-level contents" "<Shift><Control>a")
+; (gtk_accel_path "<Actions>/Tactics/Tactic jp <n>" "")
+; (gtk_accel_path "<Actions>/Templates/Template Test Printing Synth" "")
+; (gtk_accel_path "<Actions>/Tactics/Tactic set" "")
+; (gtk_accel_path "<Actions>/Edit/External editor" "")
+; (gtk_accel_path "<Actions>/View/Show Toolbar" "")
+; (gtk_accel_path "<Actions>/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/trivial" "<Primary><Control>v")
+; (gtk_accel_path "<Actions>/Tactics/Tactic fix -- with" "")
+; (gtk_accel_path "<Actions>/Tactics/Tactic pose --:=--)" "")
+; (gtk_accel_path "<Actions>/Tactics/Tactic auto with" "")
+; (gtk_accel_path "<Actions>/Templates/Template Add Printing Record" "")
+; (gtk_accel_path "<Actions>/Tactics/Tactic inversion -- in" "")
+(gtk_accel_path "<Actions>/Tactics/eauto" "<Primary><Control>e")
+; (gtk_accel_path "<Actions>/File/Open" "<Primary>o")
+; (gtk_accel_path "<Actions>/Tactics/Tactic elim -- using" "")
+; (gtk_accel_path "<Actions>/Templates/Template Hint" "")
+; (gtk_accel_path "<Actions>/Tactics/Tactic tauto" "")
+; (gtk_accel_path "<Actions>/Export/Dvi" "")
+; (gtk_accel_path "<Actions>/Tactics/Tactic simpl -- in" "")
+; (gtk_accel_path "<Actions>/Templates/Template Hint Immediate" "")
diff --git a/ide/MacOS/relatify_with-respect-to_.sh b/ide/MacOS/relatify_with-respect-to_.sh
new file mode 100755
index 00000000..a24af939
--- /dev/null
+++ b/ide/MacOS/relatify_with-respect-to_.sh
@@ -0,0 +1,15 @@
+#!/bin/sh
+
+set -e
+
+for i in "$3/"*.dylib
+do install_name_tool -change "$2"/$(basename $i) @executable_path/../Resources/lib/$(basename $i) "$1"
+done
+case "$1" in
+	*.dylib)
+	    install_name_tool -id @executable_path/../Resources/lib/$(basename $1) $1
+	    for i in "$3"/*.dylib
+	    do install_name_tool -change "$2/"$(basename $1) @executable_path/../Resources/lib/$(basename $1) $i
+	    done;;
+	*)
+esac