coq-tools
coq-tools copied to clipboard
Require resolution in the presence of passing coqc needs reworking
Since #57 was fixed, Require normalization now uses the passing coqc. However, we still look for glob files in the failing tree for everything except the bug file, which means that this interacts very poorly with the absence of --no-deps. Furthermore, it seems likely that #42 is going to cause issues. Overall, this part of the system needs to be redesigned to account for both passing and failing coqc in some coherent way.