diff options
| author |  Gregory Malecha <gmalecha@cs.harvard.edu> | 2015-08-11 12:44:29 -0700 |
|---|---|---|
| committer |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-08-13 17:13:41 +0200 |
| commit | 5cec38e8a2fbe39c75404f249974227afc028f27 (patch) | |
| tree | 468c30c8e2a324ccab70a37e8257d510ce9ba2db /tools/coqdep_common.ml | |
| parent | dda6d8f639c912597d5bf9e4f1d8c2c118b8dc48 (diff) | |
report the full module path when reporting errors in coqdep
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 8e2159745..c11113757 100644 --- a/tools/coqdep_common.ml +++ b/tools/coqdep_common.ml @@ -373,6 +373,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 -> |