aboutsummaryrefslogtreecommitdiffhomepage
path: root/tools/coqdep.ml
diff options
context:
space:
mode:
authorGravatar Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>2018-02-28 16:39:26 +0100
committerGravatar Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>2018-03-01 13:19:44 +0100
commit7e0eeba3e91cd5da029aaa6b9c86f7a13f505b88 (patch)
tree897c6504f78892b493cc4cf76593bd0417cdc549 /tools/coqdep.ml
parent195c03f798141dc816e97def7275bbdd1aa623a2 (diff)
Add source (project file / command line) to project fields.
Diffstat (limited to 'tools/coqdep.ml')
-rw-r--r--tools/coqdep.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/tools/coqdep.ml b/tools/coqdep.ml
index 4569994b4..26a2b2696 100644
--- a/tools/coqdep.ml
+++ b/tools/coqdep.ml
@@ -464,7 +464,7 @@ let split_period = Str.split (Str.regexp (Str.quote "."))
let treat_coqproject f =
let open CoqProject_file in
let project = read_project_file f in
- List.iter (treat_file None) project.v_files
+ List.iter (fun f -> treat_file None f.thing) project.v_files
let rec parse = function
| "-c" :: ll -> option_c := true; parse ll