Incorrect indentation for Coq code

[RalfJung]

In the following code, PG for some reason insists on indenting the Lemma by two spaces:

Definition dyn_reservation_map_valid_eq :
  valid = λ x, match dyn_reservation_map_token_proj x with
               | CoPset E =>
                 ✓ (dyn_reservation_map_data_proj x) ∧ set_infinite (⊤ ∖ E) ∧
                 (* dom (dyn_reservation_map_data_proj x) ⊥ E *)
                 ∀ i, dyn_reservation_map_data_proj x !! i = None ∨ i ∉ E
               | CoPsetBot => False
               end := eq_refl _.
Definition dyn_reservation_map_validN_eq :
  validN = λ n x, match dyn_reservation_map_token_proj x with
                  | CoPset E =>
                    ✓{n} (dyn_reservation_map_data_proj x) ∧ set_infinite (⊤ ∖ E) ∧
                    (* dom (dyn_reservation_map_data_proj x) ⊥ E *)
                    ∀ i, dyn_reservation_map_data_proj x !! i = None ∨ i ∉ E
                  | CoPsetBot => False
                  end := eq_refl _.

  Lemma dyn_reservation_map_included x y :
    x ≼ y ↔
      dyn_reservation_map_data_proj x ≼ dyn_reservation_map_data_proj y ∧
    dyn_reservation_map_token_proj x ≼ dyn_reservation_map_token_proj y.
  Proof.
    split; [intros [[z1 z2] Hz]; split; [exists z1|exists z2]; apply Hz|].
    intros [[z1 Hz1] [z2 Hz2]]; exists (DynReservationMap z1 z2); split; auto.
  Qed.

That does not seem right, this lemma is not nested in anything so it should not be indented.

[Matafou]

Hi, indeed this is a bug of the detection of "goal openers" of coq. I'll try to fix this scary pieace of code but meanwhile there is a workaround: put the (match... end) inside parenthesis.