Extra newline inserted after autocompletion

[jstolarek]

I say:

Goal forall n, n <= n.
  intro.
  appl

At this point company-coq offers me completion hints. I press RET to select first of them and type le_n. to get:

Goal forall n, n <= n.                                                         |
  intro.                                                                       |
  apply le_n.

Note that le_n. part is highlighted by compnay-coq as the contents of first hole to fill in. I press space but instead of simply moving one space forward company-coq inserts extra newline:

Goal forall n, n <= n.
  intro.
  apply le_n.
 X

X marks the point position. If instead of space I press RET I am moved two lines forward:

Goal forall n, n <= n.
  intro.
  apply le_n.

X

This seems to happen after every auto-completed tactic that contains arguments. I don't want any newline inserted, just the space (or a single newline if I press RET).

[jstolarek]

Minor update: this does not happen with every tactic. For example rewrite <- works fine. auto on the other hand is affected (remember that passing an argument is necessary to trigger this, so for example auto 1).

[cpitclaudel]

Sorry, I have no idea how I managed to miss this. Did you customize specific proof general options? Can you remind me which Emacs you use?

[jstolarek]

Here are my proof general settings. My Emacs is 24.5.1