The Coq mailing list

[Guillaume Melquiond <guillaume.melquiond AT inria.fr>]

Le 04/09/2020 à 04:16, Abhishek Anand a écrit :
> As shown below, the warning "br.A is required and has not been found" is
> not emitted when there is a (stray) A.vos file. 
> Is this intended? 

The same is true for stray A.vo and A.vio files. Do you think the
warning should also be emitted for those? Or do you think .vos files are
sufficiently different from .vo and .vio files to have a specific
behavior for the former?

Best regards,

Guillaume