Commit graph

3 commits

Author SHA1 Message Date
syl20bnr
8f1a5d6fd5 coq: fix some configuration
- delete some diminish expressions which are not related to PG and user
  spacemacs|hide-lighter instead of spacemacs|diminish
- move company related configuration to the correct place
- move setq expressions to :init blocks to allow users to easily change them
2017-02-12 23:45:56 -05:00
syl20bnr
fe168f07b3 coq: update key bindings and README
README:
- add `SPC m` prefixes to follow the style of the other READMEs
- Sort key bindings alphabetically

Key bindings changes made to be more mnemocnic and/or to better fit the other
key bindings of other layers:

- SPC m p b --> SPC m p p (show prover process buffer)
- SPC m p c --> SPC m p i (interrupt prover process)
- SPC m p x --> SPC m p q (quit prover process, maybe SPC m p k for kill would
  be better ?)

- SPC m a p --> SPC m a a to print query
- SPC m a n p --> SPC m a A to print query showing all
- SPC m a i p --> SPC m a i i to print query showing implicits
- Ask showing all bindings use the same keys as regular Ask but the last key
  is capitalized, example: SPC m a b (ask about) and SPC m a B (ask about
  showing all)
- Ask showing implicits are still on SPC m a i (we could also use Control key,
  for instance SPC m a b (ask about) and SPC m a C-b (ask about show implicit),
  it depends on how frequent showing implicits are used).

- SPC m g . --> SPC m g l (go to end of Locked command)
- SPC m g d --> SPC m g g (using the jump handlers facility of Spacemacs)
- SPC m g a --> SPC m g s (to go to start of command)
2017-02-12 22:24:25 -05:00
Jeremy Bi
8b72130fc5 Add coq layer 2017-02-12 21:31:44 -05:00