(************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) (* ('a -> t) * (t -> 'a) val tag : t -> string