ad6a3d0f33
refactor: deprecate featurep! for modulep!
...
featurep! will be renamed modulep! in the future, so it's been
deprecated. They have identical interfaces, and can be replaced without
issue.
featurep! was never quite the right name for this macro. It implied that
it had some connection to featurep, which it doesn't (only that it was
similar in purpose; still, Doom modules are not features). To undo such
implications and be consistent with its namespace (and since we're
heading into a storm of breaking changes with the v3 release anyway),
now was the best opportunity to begin the transition.
2022-08-14 20:43:35 +02:00
80b2071670
fix(coq): disable spinner by default
...
This was disabled upstream in
7423ee2539
2021-09-11 18:47:47 +02:00
169f9a6121
General, minor refactor & reformatting
2020-03-27 01:25:30 -04:00
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
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
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
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
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
