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
