diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-07-24 15:41:11 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-07-24 15:54:18 +0200 |
| commit | d0f9a5523bf16b18bfdf8f427b0e5f005336fa39 (patch) | |
| tree | 6f58f9d379c67ab71cce020ed15cffa15e40b573 /tools/coqdep.ml | |
| parent | 4456b5edc3e2e62624e5251ff1e01dd81fabb29b (diff) | |
Fixing bug #4265: "coqdep does not handle From ... Require" for good.
Diffstat (limited to 'tools/coqdep.ml')
| -rw-r--r-- | tools/coqdep.ml | 8 |
1 files changed, 0 insertions, 8 deletions
diff --git a/tools/coqdep.ml b/tools/coqdep.ml index ec8e983ec..99b6c7e06 100644 --- a/tools/coqdep.ml +++ b/tools/coqdep.ml @@ -36,14 +36,6 @@ let warning_mult suf iter = in iter check -let add_coqlib_known recur phys_dir log_dir f = - match get_extension f [".vo"] with - | (basename,".vo") -> - 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 sort () = let seen = Hashtbl.create 97 in let rec loop file = |