The Coq mailing list

[S�bastien Hinderer <Sebastien.Hinderer AT ens-lyon.fr>]

Dear all,

Does the Coq distribution provide a clean way to obtain, given the name of
a .v file, all the .ml files that are produced by calls to Extraction
tactic from within this file ?

It would be convenient to have such a tool, for instance during a `make
clean`, since we want to remove all .ml files produced by Extraction.

Of course, if such a tool does not exist, it should be easy enough to get
the names of the .ml files with Unix tools, but I'd like to be sure I have
to write a script, before really doing it.

Anyway, if the tool does not exist, it would probably be good to write it
and to integrate it to the Coq distribution, since the syntax of Extracsioo
will maybe change...

Thanks,
Sébastien.