[match]es sometimes screw up indentation

[coquser]

Here is some code poorly indented by TAB:

Definition foo (H : False)                                                                                                                
: H = match H return False with                                                                                                           
      end                                                                                                                                 
  := match H with end.
  Definition

The second [Definition] should not be indented.

[coquser]

Er, sorry, after a bit more experimenting, here's a better example; the first one doesn't seem to work consistently. I'm even more confused.

Definition foo0 (H : False)
: H = match H return False with
      end
:= match H with end.

  Section bar.
    Definition foo (H : False)
    : H = match H return False with
          end
      := match H with end.
    Definition baz := True.
  End bar.

  Definition qux (H : False)
  : H = match H return False with
        end
    := match H with end.

  Section quxx.
  End quxx.

The Section bar and everything after it should not be indented.