Removing dead code.

10 files changed, 0 insertions, 22 deletions

diff --git a/src/tac2core.ml b/src/tac2core.ml
index bf41713215..0415b6f15f 100644
--- a/src/tac2core.ml
+++ b/src/tac2core.ml
@@ -21,7 +21,6 @@ open Proofview.Notations
 module Value = Tac2ffi
 
 let coq_core n = KerName.make2 Tac2env.coq_prefix (Label.of_id (Id.of_string_soft n))
-let std_core n = KerName.make2 Tac2env.std_prefix (Label.of_id (Id.of_string_soft n))
 
 module Core =
 struct
diff --git a/src/tac2core.mli b/src/tac2core.mli
index d9ed8ea2e5..566b7efbb7 100644
--- a/src/tac2core.mli
+++ b/src/tac2core.mli
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Names
-open Tac2env
 open Tac2expr
 
 (** {5 Hardwired data} *)
diff --git a/src/tac2intern.ml b/src/tac2intern.ml
index bf7e93cb9e..b62a574a6c 100644
--- a/src/tac2intern.ml
+++ b/src/tac2intern.ml
@@ -24,7 +24,6 @@ let coq_type n = KerName.make2 Tac2env.coq_prefix (Label.make n)
 let t_int = coq_type "int"
 let t_string = coq_type "string"
 let t_array = coq_type "array"
-let t_unit = coq_type "unit"
 let t_list = coq_type "list"
 
 let c_nil = GTacCst (Other t_list, 0, [])
diff --git a/src/tac2intern.mli b/src/tac2intern.mli
index ddec8eb7e4..898df649ba 100644
--- a/src/tac2intern.mli
+++ b/src/tac2intern.mli
@@ -6,7 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Genarg
 open Names
 open Mod_subst
 open Tac2expr
diff --git a/src/tac2interp.mli b/src/tac2interp.mli
index bf6b2d4dde..42e9e3adeb 100644
--- a/src/tac2interp.mli
+++ b/src/tac2interp.mli
@@ -6,7 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Genarg
 open Names
 open Tac2expr
 
diff --git a/src/tac2print.mli b/src/tac2print.mli
index 2ee5cf42e0..0a04af2ff0 100644
--- a/src/tac2print.mli
+++ b/src/tac2print.mli
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Pp
-open Names
 open Tac2expr
 
 (** {5 Printing types} *)
diff --git a/src/tac2qexpr.mli b/src/tac2qexpr.mli
index a631ffd188..2e7fc7b44a 100644
--- a/src/tac2qexpr.mli
+++ b/src/tac2qexpr.mli
@@ -6,7 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Util
 open Loc
 open Names
 open Tac2expr
diff --git a/src/tac2quote.mli b/src/tac2quote.mli
index 4e563990be..456d1fa97d 100644
--- a/src/tac2quote.mli
+++ b/src/tac2quote.mli
@@ -8,7 +8,6 @@
 
 open Loc
 open Names
-open Misctypes
 open Tac2qexpr
 open Tac2expr
 
diff --git a/src/tac2stdlib.ml b/src/tac2stdlib.ml
index 3cfd0b5626..e3b0d6bf6b 100644
--- a/src/tac2stdlib.ml
+++ b/src/tac2stdlib.ml
@@ -11,8 +11,6 @@ open Locus
 open Misctypes
 open Genredexpr
 open Tac2expr
-open Tac2core
-open Tac2tactics
 open Proofview.Notations
 
 module Value = Tac2ffi
@@ -169,12 +167,6 @@ let pname s = { mltac_plugin = "ltac2"; mltac_tactic = s }
 
 let lift tac = tac <*> return v_unit
 
-let wrap f =
-  return () >>= fun () -> return (f ())
-
-let wrap_unit f =
-  return () >>= fun () -> f (); return v_unit
-
 let define_prim0 name tac =
   let tac = function
   | [_] -> lift tac
diff --git a/src/tac2tactics.ml b/src/tac2tactics.ml
index 50c1df922e..7fdda1f17d 100644
--- a/src/tac2tactics.ml
+++ b/src/tac2tactics.ml
@@ -12,11 +12,7 @@ open Globnames
 open Misctypes
 open Tactypes
 open Genredexpr
-open Tactics
 open Proofview
-open Tacmach.New
-open Tacticals.New
-open Proofview.Notations
 
 (** FIXME: export a better interface in Tactics *)
 let delayed_of_tactic tac env sigma =