The expression > match term0 return_type with pattern1 => term1 | … | patternn => termn end denotes a pattern-matching over the term term0 (expected to be of an inductive type I). The terms term1…termn are the branches of the pattern-matching expression. Each of patterni has a form qualid ident … ident where qualid must denote a constructor. There should be exactly one branch for every constructor of I. Coq < Inductive bool : Type := true : bool | false : bool. {} Coq < Inductive eq (A:Type) (x:A) : A -> Prop := eq_refl : eq A x x. {} Coq < Inductive or (A:Prop) (B:Prop) : Prop := Coq < | or_introl : A -> or A B Coq < | or_intror : B -> or A B. {} Coq < Definition bool_case (b:bool) : or (eq bool b true) (eq bool b false) Coq < := match b as x return or (eq bool x true) (eq bool x false) with Coq < | true => or_introl (eq bool true true) (eq bool true false) Coq < (eq_refl bool true) Coq < | false => or_intror (eq bool false true) (eq bool false false) Coq < (eq_refl bool false) Coq < end.