aboutsummaryrefslogtreecommitdiffhomepage
path: root/tools/coqdep.ml
diff options
context:
space:
mode:
Diffstat (limited to 'tools/coqdep.ml')
-rw-r--r--tools/coqdep.ml4
1 files changed, 0 insertions, 4 deletions
diff --git a/tools/coqdep.ml b/tools/coqdep.ml
index 2e0cce6e5..f246dc69c 100644
--- a/tools/coqdep.ml
+++ b/tools/coqdep.ml
@@ -61,7 +61,6 @@ let sort () =
try loop (Hashtbl.find vKnown s)
with Not_found -> ())
sl
- | RequireString s -> loop s
| _ -> ()
done
with Fin_fichier ->
@@ -319,9 +318,6 @@ let treat_coq_file chan =
let acc = match action with
| Require strl ->
List.fold_left mark_v_done acc strl
- | RequireString s ->
- let str = Filename.basename s in
- mark_v_done acc [str]
| Declare sl ->
let declare suff dir s =
let base = file_name s dir in