[emacs] assimilate Proof General (for Coq)
authorAmin Bandali <amin@aminb.org>
Fri, 6 Jul 2018 16:11:16 +0000 (12:11 -0400)
committerAmin Bandali <amin@aminb.org>
Fri, 6 Jul 2018 16:11:16 +0000 (12:11 -0400)
.gitmodules
init.org
lib/proof-site [new submodule]

index 165cebc..8aff0aa 100644 (file)
 [submodule "popup"]
        path = lib/popup
        url = git@github.com:auto-complete/popup-el.git
 [submodule "popup"]
        path = lib/popup
        url = git@github.com:auto-complete/popup-el.git
+[submodule "proof-site"]  # Proof General
+       path = lib/proof-site
+       url = git@github.com:ProofGeneral/PG.git
 [submodule "s"]
        path = lib/s
        url = git@github.com:magnars/s.el.git
 [submodule "s"]
        path = lib/s
        url = git@github.com:magnars/s.el.git
index bcccd39..0a61745 100644 (file)
--- a/init.org
+++ b/init.org
@@ -1091,6 +1091,13 @@ TODO: break this giant source block down into individual org sections.
   :config (setq alloy-basic-offset 2))
 #+end_src
 
   :config (setq alloy-basic-offset 2))
 #+end_src
 
+** Coq
+
+#+begin_src emacs-lisp
+(use-package proof-site  ; Proof General
+  :load-path "lib/proof-site/generic/")
+#+end_src
+
 ** [[https://github.com/leanprover/lean-mode][Lean]]
 
 #+begin_src emacs-lisp
 ** [[https://github.com/leanprover/lean-mode][Lean]]
 
 #+begin_src emacs-lisp
diff --git a/lib/proof-site b/lib/proof-site
new file mode 160000 (submodule)
index 0000000..b238dab
--- /dev/null
@@ -0,0 +1 @@
+Subproject commit b238dab7a2f8a52281a920df027c3dea4fc4b28c