coq-tools
coq-tools copied to clipboard
more robust handling of .glob files with modification times identical to .v files
The general problem with .v and .glob files having the same time is that we can't tell whether the .v file has been updated since the .glob file was generated. Fixing this requires threading through information about which files are expected to fail coqc compilation (the buggy ones only), which files must have up to date .globs even if compilation fails (the ones that the minimizer modifies), and which files we should perhaps not attempt to update the .globs on (ones in user-contrib, for example, or anything that was taken from COQPATH)