The Coq mailing list

[Guillaume Melquiond <guillaume.melquiond AT inria.fr>]

Le mardi 09 novembre 2010 à 23:10 +0100, Nikhil Swamy a écrit :
> Hi Coq-club,
> 
> Is there some way to construct a coercion in Coq based on the result
> of a pattern match? Maybe via some use of JMeq?

There is a simpler way that does not involve JMeq.

Definition bar a :=
  match a return B a -> unit with
  | One => fun b => foo b
  | Two => fun _ => tt
  end.
Print bar.

Best regards,

Guillaume