Proof Process busy on combine_split

Question

I'm doing the Software foundations exercises and doing the combine_split exercise I'm running into a wall when trying to prove an auxiliary lemma.

When applying reflexivity within the assert the Proof Process just hangs there despite the equation just being (x, y) = (x, y) which is obviously true.

Here is the implementation

Theorem combine_split : forall X Y (l : list (X * Y)) l1 l2,
  split l = (l1, l2) ->
  combine l1 l2 = l.
Proof.
  intros X Y.
  intros l.
  induction l as [| n l' IHl'].
  - simpl. intros l1 l2 H. injection H as H1 H2. rewrite <- H1, <-H2. reflexivity.
  - destruct n as [n1 n2]. simpl. destruct (split l'). 
    intros l1 l2 H. injection H as H1 H2.
    rewrite <- H1, <- H2. simpl. 
    assert ( Hc : combine x y = l'). { apply IHl'. reflexivity.} 
    apply Hc.
Qed.

Why is this happening?

Answer 1

Looks like a parsing bug in Proof General, in its sentence splitting. It appears to be sending reflexivity.} to Coq based on the highlighting when you wanted it split into reflexivity. and then } as a separate command. In any case coqc doesn't lex this as desired, interpreting .} as a single (unknown) token. (I'm actually confused why if it's sending reflexivity.} you don't get that lexing error.)

You can fix this by adding a space: reflexivity. }