diff options
| -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 } | _ |