The Coq mailing list

[Hugo Herbelin <herbelin AT pauillac.inria.fr>]

  Hi,

>  If my module contains
>  
> Require Import List Elists. 
> 
>  then coqdep misses Elists. If instead I break that line into separate
> Require Import commands, then get the correct dependencies. 

  Yes, coqdep does not support this new, still undocumented, extension
of the syntax of Require yet. It does however in the V8-0-bugfix
subversion branch downloadable from http://coq.gforge.inria.fr. Also,
a 4th patch level version of Coq 8.0 that, among other bug fixes,
includes a coqdep compatible with this feature will be made available
within a couple of weeks on the web site of Coq.

  Best regards,

  Hugo Herbelin