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_common.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_common.ml')
| -rw-r--r-- | tools/coqdep_common.ml | 11 |
1 files changed, 0 insertions, 11 deletions
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 |