diff options
author | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-01-29 17:27:49 +0100 |
---|---|---|
committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-01-29 18:03:50 +0100 |
commit | 0b644da20c714b01565f88dffcfd51ea8f08314a (patch) | |
tree | 5a63fe126f7ae1f5d0e9460234291dd3dd55a78b /tools/coqdep_common.ml | |
parent | 4953a129858a231e64dec636a3bc15a54a0e771c (diff) | |
parent | 22a2cc1897f0d9f568ebfb807673e84f6ada491a (diff) |
Merge branch 'v8.5'
Diffstat (limited to 'tools/coqdep_common.ml')
-rw-r--r-- | tools/coqdep_common.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/tools/coqdep_common.ml b/tools/coqdep_common.ml index f5eccbfa4..c63e4aaa6 100644 --- a/tools/coqdep_common.ml +++ b/tools/coqdep_common.ml @@ -489,15 +489,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 @@ -506,7 +506,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 |