"coqdep" -I . -c "purify_tactic_plugin.mllib" > "purify_tactic_plugin.mllib.d" || ( RV=$?; rm -f "purify_tactic_plugin.mllib.d"; exit $RV )
*** Warning: purify_tactic_plugin.mllib already found in . (discarding ./purify_tactic_plugin.mllib)