Commit Graph

34 Commits

Author SHA1 Message Date
8a5ffc32f5 Bump to ProofGeneral/PG@2a17093
From ProofGeneral/PG@89829c2

Also removes pg-init hacks, as they no longer seem necessary after
ProofGeneral/PG@7371521

Hopefully fixes #2565
2020-02-20 16:55:19 -05:00
a9402cfb55 Fix #2373: bring back package pinning
This needs some serious refactoring...
2020-01-25 19:02:00 -05:00
4cc14389e8 PIN ALL THE PACKAGES 2020-01-14 22:32:11 -05:00
566d54d984 Disable continue-comments-on-RET in ess-r-mode & coq-mode
Fixes #2081, #2233
2019-12-27 13:32:24 -05:00
a4e9d85db4 invert (if (not ..)) statement 2019-11-17 01:22:12 +09:00
c4fad17c29 Remove company-coq's hello page 2019-11-17 01:21:39 +09:00
78bb2e2ae5 diable the hello feature of company-coq 2019-11-17 00:34:15 +09:00
5738e39fea Disable proof general's splash screen 2019-11-17 00:33:52 +09:00
8eb9cf5b30 lang/coq: setup company ourselves + minor refactor
company-coq imposes its own value for company-idle-delay, potentially
overriding the user's customizations, so we set up company ourselves.
2019-10-21 09:01:49 -04:00
42624c8090 [coq] disable electric proof terminators
These send input to coq too agressively. It's often the case that this
causes delays in coq.

Signed-off-by: Rudi Grinberg <rudi.grinberg@gmail.com>
2019-10-20 14:37:35 +09:00
22ae9cca15 lang/coq: tab-width = proof-indent 2019-10-19 04:00:27 -04:00
c21607ae66 lang/coq: general refactor
Potentially fixes #1854
2019-10-04 15:33:37 -04:00
f68203c2ef lang/coq: fix file-missing proof-site errors
Occasionally happens after the first time running `doom refresh` (after
installing proof-general).
2019-10-03 11:43:16 -04:00
081e57dc10 Add coq key bindings
These bindings are modelled afer the bindings in spacemacs

Signed-off-by: Rudi Grinberg <rudi.grinberg@gmail.com>
2019-09-08 17:44:12 +09:00
62af55dad0 Move emacs-snippets -> doom-snippets
The repo was renamed upstream.
2019-07-14 17:05:48 +02:00
7c9e96da87 General module refactor 2019-03-02 02:04:11 -05:00
84af639fc3 set-popup-rules! -> set-popup-rule!
Semantic refactor.

Also adjusts regexp to use non-capturing group (for slight performance benefit).
2018-12-03 22:23:57 -05:00
dcbcc4d1e7 Added a popup rule to ignore proof general popups 2018-12-02 13:22:42 -05:00
b89fcd8726 Replace Coq-Mode abbreviations with yasnippet
Since ProofGenerals abbreviation usage interfers with
evil-mode, this empties the abbreviation table of coq-mode.
The abbreviations got transformed into yasnippet snippets
and put into hlissner/emacs-snippets#4.
2018-10-07 09:18:25 +02:00
5bfaabd99b Proof-general is now on melpa 2018-09-06 01:29:01 +02:00
f75381ae51 when not => unless 2018-08-31 03:32:25 +02:00
f95623989d lang/coq: remove unnecessary after!
For setting a variable, an after! block is overkill
2018-08-31 03:31:58 +02:00
953906ccdb Terminator triggers evaluation 2018-08-27 15:35:18 +02:00
f6e9b943fd Change ref function 2018-08-27 14:11:14 +02:00
5492315053 Added lookup handlers 2018-08-27 13:57:00 +02:00
d9f819dac4 Only make company features conditional 2018-08-27 12:57:07 +02:00
dbca4eef12 Put company features behind conditional 2018-08-21 13:44:11 +02:00
48c531e76c lang/coq: move config.el to autoload.el
The auto-mode-alist entry for coq-mode and friends are already added by proof-general's autoloads file, and neither coq-mode nor company-coq-mode belong to proof-site specifically, so they shouldn't be treated like they are (this could cause autoloading errors).

The `def-package!` block altogether is unnecessary. The only thing we need is to enable `company-coq-mode` on coq-mode-hook. However, having a one-line config.el is a tad excessive, so we put it in autoload.el instead.
2018-08-18 23:45:36 +02:00
6393ebe16b Removed redundant config 2018-08-18 14:51:21 +02:00
55b5c7711b Updated readme 2018-08-15 08:34:21 +02:00
f5c1be44ba Added quelpa recipe 2018-08-15 08:33:38 +02:00
2929b58cde Modified variable 2018-08-15 08:17:20 +02:00
4280ea3418 Added readme. 2018-08-14 23:30:20 +02:00
fa223ceafd Added basic coq support 2018-08-14 23:21:55 +02:00