Dead code in extraction

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

8 files changed, 0 insertions, 60 deletions

diff --git a/plugins/extraction/common.ml b/plugins/extraction/common.ml
index 35d7ba3d5..61e2f8c28 100644
--- a/plugins/extraction/common.ml
+++ b/plugins/extraction/common.ml
@@ -45,8 +45,6 @@ let fnl2 () = fnl () ++ fnl ()
 
 let space_if = function true -> str " " | false -> mt ()
 
-let sec_space_if = function true -> spc () | false -> mt ()
-
 let is_digit = function
   | '0'..'9' -> true
   | _ -> false
diff --git a/plugins/extraction/common.mli b/plugins/extraction/common.mli
index e85201982..0abb47c22 100644
--- a/plugins/extraction/common.mli
+++ b/plugins/extraction/common.mli
@@ -14,7 +14,6 @@ open Pp
 
 val fnl2 : unit -> std_ppcmds
 val space_if : bool -> std_ppcmds
-val sec_space_if : bool -> std_ppcmds
 
 val pp_par : bool -> std_ppcmds -> std_ppcmds
 val pp_apply : std_ppcmds -> bool -> std_ppcmds list -> std_ppcmds
diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index ba7fc272a..1e2793aa5 100644
--- a/plugins/extraction/extraction.ml
+++ b/plugins/extraction/extraction.ml
@@ -38,8 +38,6 @@ let type_of env c = Retyping.get_type_of env none (strip_outer_cast c)
 
 let sort_of env c = Retyping.get_sort_family_of env none (strip_outer_cast c)
 
-let is_axiom env kn = (Environ.lookup_constant kn env).const_body = None
-
 (*S Generation of flags and signatures. *)
 
 (* The type [flag] gives us information about any Coq term:
@@ -272,14 +270,6 @@ let rec extract_type env db j c args =
     | Case _ | Fix _ | CoFix _ -> Tunknown
     | _ -> assert false
 
-(* [extract_maybe_type] calls [extract_type] when used on a Coq type,
-   and otherwise returns [Tdummy] or [Tunknown] *)
-
-and extract_maybe_type env db c =
-  let t = whd_betadeltaiota env none (type_of env c) in
-  if isSort t then extract_type env db 0 c []
-  else if sort_of env t = InProp then Tdummy Kother else Tunknown
-
 (*s Auxiliary function dealing with type application.
   Precondition: [r] is a type scheme represented by the signature [s],
   and is completely applied: [List.length args = List.length s]. *)
diff --git a/plugins/extraction/haskell.ml b/plugins/extraction/haskell.ml
index 3048db4b7..3d18431aa 100644
--- a/plugins/extraction/haskell.ml
+++ b/plugins/extraction/haskell.ml
@@ -281,8 +281,6 @@ let rec pp_ind first kn i ind =
 
 (*s Pretty-printing of a declaration. *)
 
-let pp_string_parameters ids = prlist (fun id -> str id ++ str " ")
-
 let pp_decl = function
   | Dind (kn,i) when i.ind_info = Singleton ->
       pp_singleton (mind_of_kn kn) i.ind_packets.(0) ++ fnl ()
diff --git a/plugins/extraction/mlutil.ml b/plugins/extraction/mlutil.ml
index e8f852266..29f9a817d 100644
--- a/plugins/extraction/mlutil.ml
+++ b/plugins/extraction/mlutil.ml
@@ -54,18 +54,6 @@ let new_meta _ =
   incr meta_count;
   Tmeta {id = !meta_count; contents = None}
 
-(*s Sustitution of [Tvar i] by [t] in a ML type. *)
-
-let type_subst i t0 t =
-  let rec subst t = match t with
-    | Tvar j when i = j -> t0
-    | Tmeta {contents=None} -> t
-    | Tmeta {contents=Some u} -> subst u
-    | Tarr (a,b) -> Tarr (subst a, subst b)
-    | Tglob (r, l) -> Tglob (r, List.map subst l)
-    | a -> a
-  in subst t
-
 (* Simultaneous substitution of [[Tvar 1; ... ; Tvar n]] by [l] in a ML type. *)
 
 let type_subst_list l t =
@@ -441,15 +429,6 @@ let ast_occurs_itvl k k' t =
     ast_iter_rel (fun i -> if (k <= i) && (i <= k') then raise Found) t; false
   with Found -> true
 
-(*s Number of occurences of [Rel k] (resp. [Rel 1]) in [t]. *)
-
-let nb_occur_k k t =
-  let cpt = ref 0 in
-  ast_iter_rel (fun i -> if i = k then incr cpt) t;
-  !cpt
-
-let nb_occur t = nb_occur_k 1 t
-
 (* Number of occurences of [Rel 1] in [t], with special treatment of match:
    occurences in different branches aren't added, but we rather use max. *)
 
@@ -572,7 +551,6 @@ let rec many_lams id a = function
   | 0 -> a
   | n -> many_lams id (MLlam (id,a)) (pred n)
 
-let anonym_lams a n = many_lams anonymous a n
 let anonym_tmp_lams a n = many_lams (Tmp anonymous_name) a n
 let dummy_lams a n = many_lams Dummy a n
 
@@ -1144,11 +1122,6 @@ and ml_size_array l = Array.fold_left (fun a t -> a + ml_size t) 0 l
 
 let is_fix = function MLfix _ -> true | _ -> false
 
-let rec is_constr = function
-  | MLcons _   -> true
-  | MLlam(_,t) -> is_constr t
-  | _          -> false
-
 (*s Strictness *)
 
 (* A variable is strict if the evaluation of the whole term implies
diff --git a/plugins/extraction/mlutil.mli b/plugins/extraction/mlutil.mli
index 022e42fdd..b4f3c4c18 100644
--- a/plugins/extraction/mlutil.mli
+++ b/plugins/extraction/mlutil.mli
@@ -18,7 +18,6 @@ open Table
 val reset_meta_count : unit -> unit
 val new_meta : 'a -> ml_type
 
-val type_subst : int -> ml_type -> ml_type -> ml_type
 val type_subst_list : ml_type list -> ml_type -> ml_type
 val type_subst_vect : ml_type array -> ml_type -> ml_type
 
diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml
index a292dec2f..c1b488f35 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, ... *)
 
diff --git a/plugins/extraction/table.mli b/plugins/extraction/table.mli
index a0cffa596..f55ae53d8 100644
--- a/plugins/extraction/table.mli
+++ b/plugins/extraction/table.mli
@@ -56,10 +56,8 @@ val at_toplevel : module_path -> bool
 val visible_con : constant -> bool
 val mp_length : module_path -> int
 val prefixes_mp : module_path -> MPset.t
-val modfile_of_mp : module_path -> module_path
 val common_prefix_from_list :
   module_path -> module_path list -> module_path option
-val add_labels_mp : module_path -> label list -> module_path
 val get_nth_label_mp : int -> module_path -> label
 val labels_of_ref : global_reference -> module_path * label list