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 *)
  intros n. destruct n.
  - simpl. reflexivity.
  - simpl. simpl beta delta [] iota zeta. 

1 Answer 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.

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.