diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-06-30 16:47:28 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-06-30 16:49:15 +0200 |
| commit | 72f128af5a00e5509239e46b395c9cd10e53b36a (patch) | |
| tree | f0b9aecae361704b534abf45ebc63a1cabd5c3fb /tools/coqdep.ml | |
| parent | 2defd4c15467736b73f69adb501e3a4fe2111ce5 (diff) | |
Removing dead code in coqdep.
Since commit 2f521670fbd, the Require "file" syntax was not used anymore by
coqtop but the code handling it was still there in coqdep. We finish the work
by erasing the remnant code.
Diffstat (limited to 'tools/coqdep.ml')
| -rw-r--r-- | tools/coqdep.ml | 4 |
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 |