0

This might be a strange question but every time I type:

simpl. <ESC>

Evil substitutes it with:

simpl beta delta [] iota zeta.

this is driving me nuts. Why is this happening and more importantely, how do I stop it? I want to be able to escape Vim's insert mode without it doing some weird auto complete.

Note I am using ProofGeneral because I happen to be working with Coq.

For context my code:

Theorem zero_nbeq_S : forall n:nat,
  beq_nat 0 (S n) = false. (* 0 = S n ~ false *)
Proof.
  intros n. destruct n.
  - simpl. reflexivity.
  - simpl. simpl beta delta [] iota zeta. 
Qed.
Charlie Parker
  • 121
  • 6

1 Answers1

1

This is abbrev, a way of expanding an abbreviation to a longer snippet of text. To trigger one, you must type a key that cannot possibly be part of the abbreviation, like SPC or ESC. See https://github.com/ProofGeneral/PG/blob/fb3b75dab55b6e6befffc53e136422558be5faa0/coq/coq-syntax.el#L287 and https://github.com/ProofGeneral/PG/blob/1854459fef368dfc8ca870792e7e3b065a2241c6/coq/coq-abbrev.el#L39-L40 where it's set up.

To disable this behavior for ESC, customize evil-want-abbrev-expand-on-insert-exit.

wasamasa
  • 21,803
  • 1
  • 65
  • 97