Add 'as' and 'return' keywords in 'match ... with' constructions

[lgeorget]

Hello!

In this small patch, I add the keywords 'as' and 'return' to various 'match ... with' constructions. It is used in this kind of constructions:

Definition pred_partial : forall n:nat, n <> 0 -> nat.
  refine
  (fun n =>
    match n as x return x <> 0 -> nat with
    | O => fun h:0 <> 0 => _
    | S p => fun h:S p <> 0 => p
  end).
  elim h.
  reflexivity.
Defined.

(Taken from the Coq'Art, by Yves Bertot and Pierre Castéran, https://www.labri.fr/perso/casteran/CoqArt/coqartF.pdf).

[lgeorget]

For those who are interested, the previous definition is equivalent to:

Definition pred_partial' : forall n:nat, n <> 0 -> nat :=
  fun n =>
    match n as x return x <> 0 -> nat with
    | O => fun h:0 <> 0 => False_rec nat (h eq_refl)
    | S p => fun h:S p <> 0 => p
  end.

[trefis]

Thank you!