diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-08-22 16:21:07 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-08-22 16:21:07 +0200 |
| commit | 2903ee1394118106f1894798f82dc5cf3730675b (patch) | |
| tree | 76a29b8da20b51b48c6a73516a6ae9c107f57afc /tools/coqdep_common.ml | |
| parent | 4c202177e7d1a26f3b8bc105a1ceb604f178b584 (diff) | |
| parent | 081a649157d2460c924404cd51b4ba50c23b1956 (diff) | |
Merge branch 'v8.5'
Diffstat (limited to 'tools/coqdep_common.ml')
| -rw-r--r-- | tools/coqdep_common.ml | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/tools/coqdep_common.ml b/tools/coqdep_common.ml index 967ec419f..2cdb66aa7 100644 --- a/tools/coqdep_common.ml +++ b/tools/coqdep_common.ml @@ -363,6 +363,11 @@ let rec traite_fichier_Coq suffixe verbose f = printf " %s%s" (canonize file_str) suffixe with Not_found -> if verbose && not (is_in_coqlib ?from str) then + let str = + match from with + | None -> str + | Some pth -> pth @ str + in warning_module_notfound f str end) strl | Declare sl -> |