From 72f128af5a00e5509239e46b395c9cd10e53b36a Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>
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.ml        |  4 ----
 tools/coqdep_common.ml | 11 -----------
 tools/coqdep_lexer.mli |  1 -
 tools/coqdep_lexer.mll |  5 -----
 4 files changed, 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 }
   | _
-- 
cgit v1.2.3