This might be a strange question but every time I type:
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.