coq-tools icon indicating copy to clipboard operation
coq-tools copied to clipboard

Require resolution in the presence of passing coqc needs reworking

Open JasonGross opened this issue 4 years ago • 0 comments

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.

JasonGross avatar May 24 '21 12:05 JasonGross