aboutsummaryrefslogtreecommitdiffhomepage
path: root/tools/coqdep_common.ml
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2016-01-24 16:25:38 +0100
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2016-01-24 16:34:02 +0100
commitf17096fa9eff103f40e6d381ebeb4313002fa378 (patch)
treeb7eed322565fd51f282872194d688863a70bd4eb /tools/coqdep_common.ml
parent030ef2f015e5c592ea7599f0f98a715873c1e4d0 (diff)
Fixing bug #4373: coqdep does not know about .vio files.
Diffstat (limited to 'tools/coqdep_common.ml')
-rw-r--r--tools/coqdep_common.ml8
1 files changed, 4 insertions, 4 deletions
diff --git a/tools/coqdep_common.ml b/tools/coqdep_common.ml
index 58c8e884c..a90264e26 100644
--- a/tools/coqdep_common.ml
+++ b/tools/coqdep_common.ml
@@ -504,15 +504,15 @@ let add_caml_known phys_dir _ f =
| _ -> ()
let add_coqlib_known recur phys_dir log_dir f =
- match get_extension f [".vo"] with
- | (basename,".vo") ->
+ match get_extension f [".vo"; ".vio"] with
+ | (basename, (".vo" | ".vio")) ->
let name = log_dir@[basename] in
let paths = if recur then suffixes name else [name] in
List.iter (fun f -> Hashtbl.add coqlibKnown f ()) paths
| _ -> ()
let add_known recur phys_dir log_dir f =
- match get_extension f [".v";".vo"] with
+ match get_extension f [".v"; ".vo"; ".vio"] with
| (basename,".v") ->
let name = log_dir@[basename] in
let file = phys_dir//basename in
@@ -521,7 +521,7 @@ let add_known recur phys_dir log_dir f =
let paths = List.tl (suffixes name) in
let iter n = safe_hash_add compare_file clash_v vKnown (n, (file, false)) in
List.iter iter paths
- | (basename,".vo") when not(!option_boot) ->
+ | (basename, (".vo" | ".vio")) when not(!option_boot) ->
let name = log_dir@[basename] in
let paths = if recur then suffixes name else [name] in
List.iter (fun f -> Hashtbl.add coqlibKnown f ()) paths