Henrik Lissner
d03ac051bf
fix(coq): inhibit indent detection
...
Indent detection (via dtrt-indent) is slow and inconclusive in coq-mode
files. Since it's rarely helpful for them anyway, I inhibit it.
Fix : #5823
2024-02-02 03:33:53 -05:00
Henrik Lissner
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
Tej Chajed
80b2071670
fix(coq): disable spinner by default
...
This was disabled upstream in
7423ee2539
2021-09-11 18:47:47 +02:00
Henrik Lissner
169f9a6121
General, minor refactor & reformatting
2020-03-27 01:25:30 -04:00
Henrik Lissner
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
Henrik Lissner
566d54d984
Disable continue-comments-on-RET in ess-r-mode & coq-mode
...
Fixes #2081 , #2233
2019-12-27 13:32:24 -05:00
Rudi Grinberg
a4e9d85db4
invert (if (not ..)) statement
2019-11-17 01:22:12 +09:00
Rudi Grinberg
c4fad17c29
Remove company-coq's hello page
2019-11-17 01:21:39 +09:00
Rudi Grinberg
78bb2e2ae5
diable the hello feature of company-coq
2019-11-17 00:34:15 +09:00
Rudi Grinberg
5738e39fea
Disable proof general's splash screen
2019-11-17 00:33:52 +09:00
Henrik Lissner
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
Rudi Grinberg
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
Henrik Lissner
22ae9cca15
lang/coq: tab-width = proof-indent
2019-10-19 04:00:27 -04:00
Henrik Lissner
c21607ae66
lang/coq: general refactor
...
Potentially fixes #1854
2019-10-04 15:33:37 -04:00
Rudi Grinberg
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
Henrik Lissner
7c9e96da87
General module refactor
2019-03-02 02:04:11 -05:00
Henrik Lissner
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
Elijah Malaby
dcbcc4d1e7
Added a popup rule to ignore proof general popups
2018-12-02 13:22:42 -05:00
Sebastian Wild
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
Henrik Lissner
f75381ae51
when not => unless
2018-08-31 03:32:25 +02:00
Henrik Lissner
f95623989d
lang/coq: remove unnecessary after!
...
For setting a variable, an after! block is overkill
2018-08-31 03:31:58 +02:00
Patrick Elliott
953906ccdb
Terminator triggers evaluation
2018-08-27 15:35:18 +02:00
Patrick Elliott
f6e9b943fd
Change ref function
2018-08-27 14:11:14 +02:00
Patrick Elliott
5492315053
Added lookup handlers
2018-08-27 13:57:00 +02:00
Patrick Elliott
d9f819dac4
Only make company features conditional
2018-08-27 12:57:07 +02:00
