From 72f128af5a00e5509239e46b395c9cd10e53b36a Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 30 Jun 2015 16:47:28 +0200 Subject: 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. --- tools/coqdep_common.ml | 11 ----------- 1 file changed, 11 deletions(-) (limited to 'tools/coqdep_common.ml') diff --git a/tools/coqdep_common.ml b/tools/coqdep_common.ml index d86e05d8c..743853738 100644 --- a/tools/coqdep_common.ml +++ b/tools/coqdep_common.ml @@ -326,17 +326,6 @@ let rec traite_fichier_Coq suffixe verbose f = if verbose && not (Hashtbl.mem coqlibKnown str) then warning_module_notfound f str end) strl - | RequireString s -> - let str = Filename.basename s in - if not (List.mem [str] !deja_vu_v) then begin - addQueue deja_vu_v [str]; - try - let file_str = Hashtbl.find vKnown [str] in - printf " %s%s" (canonize file_str) suffixe - with Not_found -> - if not (Hashtbl.mem coqlibKnown [str]) then - warning_notfound f s - end | Declare sl -> let declare suff dir s = let base = file_name s dir in -- cgit v1.2.3