(***********************************************************************) (* *) (* Compcert Extensions *) (* *) (* Jean-Baptiste Tristan *) (* *) (* All rights reserved. This file is distributed under the terms *) (* described in file ../../LICENSE. *) (* *) (***********************************************************************) val type_function : RTL.coq_function -> unit