still some more dead code removal

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

4 files changed, 3 insertions, 29 deletions

diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index a14b47393..533fbfaaa 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -15,25 +15,6 @@ open Misctypes
 exception Toberemoved_with_rel of int*constr
 exception Toberemoved
 
-
-let pr_elim_scheme el =
-  let env = Global.env () in
-  let msg = str "params := " ++ Printer.pr_rel_context env el.params in
-  let env = Environ.push_rel_context el.params env in
-  let msg = msg ++ fnl () ++ str "predicates := "++ Printer.pr_rel_context env el.predicates in
-  let env = Environ.push_rel_context el.predicates env in
-  let msg = msg ++ fnl () ++ str "branches := " ++ Printer.pr_rel_context env el.branches in
-  let env = Environ.push_rel_context el.branches env in
-  let msg = msg ++ fnl () ++ str "args := " ++ Printer.pr_rel_context env el.args in
-  let env = Environ.push_rel_context el.args env in
-  msg ++ fnl () ++ str "concl := " ++ pr_lconstr_env env el.concl
-
-
-let observe s =
-  if do_observe ()
-  then Pp.msg_debug s
-
-
 let pr_elim_scheme el =
   let env = Global.env () in
   let msg = str "params := " ++ Printer.pr_rel_context env el.params in
diff --git a/plugins/micromega/csdpcert.ml b/plugins/micromega/csdpcert.ml
index e416c514c..f848591cc 100644
--- a/plugins/micromega/csdpcert.ml
+++ b/plugins/micromega/csdpcert.ml
@@ -12,7 +12,6 @@
 (*                                                                      *)
 (************************************************************************)
 
-open Big_int
 open Num
 open Sos
 open Sos_types
@@ -60,7 +59,7 @@ open Mutils
 
 
 
-let rec canonical_sum_to_string = function s -> failwith "not implemented"
+let canonical_sum_to_string = function s -> failwith "not implemented"
 
 let print_canonical_sum m = Format.print_string (canonical_sum_to_string m)
 
diff --git a/plugins/micromega/sos_lib.ml b/plugins/micromega/sos_lib.ml
index e592611ac..41cbeda3f 100644
--- a/plugins/micromega/sos_lib.ml
+++ b/plugins/micromega/sos_lib.ml
@@ -6,7 +6,7 @@
 (*   independent bits                                                        *)
 (* - Frédéric Besson (fbesson@irisa.fr) is using it to feed  micromega       *)
 (* ========================================================================= *)
-open Sos_types
+
 open Num
 
 let debugging = ref false;;
@@ -546,7 +546,7 @@ let fix err prs input =
   try prs input
   with Noparse -> failwith (err ^ " expected");;
 
-let rec listof prs sep err =
+let listof prs sep err =
   prs ++ many (sep ++ fix err prs >> snd) >> (fun (h,t) -> h::t);;
 
 let possibly prs input =
diff --git a/plugins/xml/xmlcommand.ml b/plugins/xml/xmlcommand.ml
index 0673e79fb..8259266af 100644
--- a/plugins/xml/xmlcommand.ml
+++ b/plugins/xml/xmlcommand.ml
@@ -108,12 +108,6 @@ let types_filename_of_filename =
   | None   -> None
 ;;
 
-let prooftree_filename_of_filename =
- function
-    Some f -> Some (f ^ ".proof_tree")
-  | None   -> None
-;;
-
 let theory_filename xml_library_root =
  let module N = Names in
   match xml_library_root with