Removing dead code.

5 files changed, 0 insertions, 23 deletions

diff --git a/plugins/cc/ccproof.ml b/plugins/cc/ccproof.ml
index 4e1806f5a..6177f22f3 100644
--- a/plugins/cc/ccproof.ml
+++ b/plugins/cc/ccproof.ml
@@ -10,7 +10,6 @@
 (* proof-trees that will be transformed into proof-terms in cctac.ml4   *)
 
 open Errors
-open Names
 open Term
 open Ccalgo
 
diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml
index 2de0fe717..73c050bb2 100644
--- a/plugins/cc/cctac.ml
+++ b/plugins/cc/cctac.ml
@@ -468,8 +468,6 @@ let congruence_tac depth l =
    might be slow now, let's rather do something equivalent
    to a "simple apply refl_equal" *)
 
-let simple_reflexivity () = apply (Universes.constr_of_global _refl_equal)
-
 (* The [f_equal] tactic.
 
    It mimics the use of lemmas [f_equal], [f_equal2], etc.
diff --git a/plugins/firstorder/instances.ml b/plugins/firstorder/instances.ml
index 11b120c41..076107450 100644
--- a/plugins/firstorder/instances.ml
+++ b/plugins/firstorder/instances.ml
@@ -21,7 +21,6 @@ open Reductionops
 open Formula
 open Sequent
 open Names
-open Globnames
 open Misctypes
 
 let compare_instance inst1 inst2=
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index f4a062732..8c3033d0c 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -17,19 +17,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
@@ -270,10 +257,6 @@ let change_property_sort toSort princ princName =
     )
     princ_info.params
 
-
-let pp_dur time time' =
-  str (string_of_float (System.time_difference time time'))
-
 let build_functional_principle interactive_proof old_princ_type sorts funs i proof_tac hook =
   (* First we get the type of the old graph principle *)
   let mutr_nparams = (compute_elim_sig old_princ_type).nparams in
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index d8f006f51..961266c9c 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -10,7 +10,6 @@ open Term
 open Vars
 open Namegen
 open Environ
-open Declareops
 open Entries
 open Pp
 open Names
@@ -125,7 +124,6 @@ let lt = function () -> (coq_base_constant "lt")
 let le = function () -> (coq_base_constant "le")
 let ex = function () -> (coq_base_constant "ex")
 let nat = function () -> (coq_base_constant "nat")
-let coq_sig = function () -> (coq_base_constant "sig")
 let iter_ref () =  
   try find_reference ["Recdef"] "iter" 
   with Not_found -> error "module Recdef not loaded"