CFML is not a computer language. It's two things: (1) a program that takes as input an ML program (more precisely a Caml program, i.e. Ocaml without objects) an

CFML is not a computer language. It's two things: (1) a program that takes as input an ML program (more precisely a Caml program, i.e. Ocaml without objects) and computes the characteristic formula (expressed in the logic of Coq) of the program; (2) a Coq library, more precisely a library of Coq tactics, that enables users interactively to manipulate characteristic formulae of Caml programs in Coq. So Charguéraud's CFML is far away from cold fusion that context can always disambiguate. And if not ... is the sky going to fall down?