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