Dead code in extraction

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13461 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 0 insertions, 15 deletions

diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml
index a292dec2f9..c1b488f350 100644
--- a/plugins/extraction/table.ml
+++ b/plugins/extraction/table.ml
@@ -58,11 +58,6 @@ let raw_string_of_modfile = function
   | MPfile f -> String.capitalize (string_of_id (List.hd (repr_dirpath f)))
   | _ -> assert false
 
-let rec modfile_of_mp = function
-  | (MPfile _) as mp -> mp
-  | MPdot (mp,_) -> modfile_of_mp mp
-  | _ -> raise Not_found
-
 let current_toplevel () = fst (Lib.current_prefix ())
 
 let is_toplevel mp =
@@ -96,12 +91,6 @@ let common_prefix_from_list mp0 mpl =
     | mp :: l -> if MPset.mem mp prefixes then Some mp else f l
   in f mpl
 
-let rec parse_labels ll = function
-  | MPdot (mp,l) -> parse_labels (l::ll) mp
-  | mp -> mp,ll
-
-let labels_of_mp mp = parse_labels [] mp
-
 let rec parse_labels2 ll mp1 = function
   | mp when mp1=mp -> mp,ll
   | MPdot (mp,l) -> parse_labels2 (l::ll) mp1 mp
@@ -112,10 +101,6 @@ let labels_of_ref r =
   let mp,_,l = repr_of_r r in
   parse_labels2 [l] mp_top mp
 
-let rec add_labels_mp mp = function
-  | [] -> mp
-  | l :: ll -> add_labels_mp (MPdot (mp,l)) ll
-
 
 (*S The main tables: constants, inductives, records, ... *)