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 | |
| 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.
| -rw-r--r-- | tools/coqdep.ml | 4 | ||||
| -rw-r--r-- | tools/coqdep_common.ml | 11 | ||||
| -rw-r--r-- | tools/coqdep_lexer.mli | 1 | ||||
| -rw-r--r-- | tools/coqdep_lexer.mll | 5 |
4 files changed, 0 insertions, 21 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 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 diff --git a/tools/coqdep_lexer.mli b/tools/coqdep_lexer.mli index b447030af..c7b9c9a0a 100644 --- a/tools/coqdep_lexer.mli +++ b/tools/coqdep_lexer.mli @@ -12,7 +12,6 @@ type qualid = string list type coq_token = Require of qualid list - | RequireString of string | Declare of string list | Load of string | AddLoadPath of string diff --git a/tools/coqdep_lexer.mll b/tools/coqdep_lexer.mll index 8ecc419c8..5692e5b45 100644 --- a/tools/coqdep_lexer.mll +++ b/tools/coqdep_lexer.mll @@ -17,7 +17,6 @@ type coq_token = | Require of qualid list - | RequireString of string | Declare of string list | Load of string | AddLoadPath of string @@ -277,10 +276,6 @@ and require_file = parse | Some from -> (from_pre_ident := None ; Require (List.map (fun x -> from @ x) qid)) } - | '"' [^'"']* '"' (*'"'*) - { let s = Lexing.lexeme lexbuf in - parse_dot lexbuf; - RequireString (unquote_vfile_string s) } | eof { syntax_error lexbuf } | _ |