(************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) (* bool) -> 'a -> 'a