From 533b5ee5a3c5dd4c2e54d85dba9485722bb21db1 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sat, 7 Oct 2017 22:47:48 +0200
Subject: Remove unused warnings.

---
 src/tac2core.ml    | 4 ----
 src/tac2entries.ml | 1 -
 src/tac2env.ml     | 2 --
 src/tac2env.mli    | 1 -
 src/tac2expr.mli   | 1 -
 src/tac2ffi.ml     | 1 -
 src/tac2intern.ml  | 6 ------
 src/tac2interp.ml  | 1 -
 src/tac2print.ml   | 1 -
 src/tac2quote.ml   | 2 --
 src/tac2quote.mli  | 1 -
 src/tac2stdlib.ml  | 2 --
 src/tac2tactics.ml | 2 --
 13 files changed, 25 deletions(-)

(limited to 'src')

diff --git a/src/tac2core.ml b/src/tac2core.ml
index 1489c50c13..0304286639 100644
--- a/src/tac2core.ml
+++ b/src/tac2core.ml
@@ -6,13 +6,11 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open CSig
 open Util
 open Pp
 open Names
 open Genarg
 open Tac2env
-open Tac2dyn
 open Tac2expr
 open Tac2entries.Pltac
 open Proofview.Notations
@@ -105,7 +103,6 @@ let err_matchfailure =
 let thaw f = Tac2ffi.apply f [v_unit]
 
 let fatal_flag : unit Exninfo.t = Exninfo.make ()
-let fatal_info = Exninfo.add Exninfo.null fatal_flag ()
 
 let set_bt info =
   if !Tac2interp.print_ltac2_backtrace then
@@ -397,7 +394,6 @@ let () = define1 "constr_kind" constr begin fun c ->
 end
 
 let () = define1 "constr_make" valexpr begin fun knd ->
-  let open Constr in
   let c = match Tac2ffi.to_block knd with
   | (0, [|n|]) ->
     let n = Value.to_int n in
diff --git a/src/tac2entries.ml b/src/tac2entries.ml
index cd4b701ca7..f24c409ad7 100644
--- a/src/tac2entries.ml
+++ b/src/tac2entries.ml
@@ -16,7 +16,6 @@ open Nametab
 open Tac2expr
 open Tac2print
 open Tac2intern
-open Vernacexpr
 
 (** Grammar entries *)
 
diff --git a/src/tac2env.ml b/src/tac2env.ml
index 0aa2da77ae..2f1124c156 100644
--- a/src/tac2env.ml
+++ b/src/tac2env.ml
@@ -6,11 +6,9 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open CErrors
 open Util
 open Names
 open Libnames
-open Tac2dyn
 open Tac2expr
 open Tac2ffi
 
diff --git a/src/tac2env.mli b/src/tac2env.mli
index b82923765d..022c518143 100644
--- a/src/tac2env.mli
+++ b/src/tac2env.mli
@@ -10,7 +10,6 @@ open Genarg
 open Names
 open Libnames
 open Nametab
-open Tac2dyn
 open Tac2expr
 open Tac2ffi
 
diff --git a/src/tac2expr.mli b/src/tac2expr.mli
index c787870c65..e57b0ba3ef 100644
--- a/src/tac2expr.mli
+++ b/src/tac2expr.mli
@@ -7,7 +7,6 @@
 (************************************************************************)
 
 open Loc
-open Genarg
 open Names
 open Libnames
 
diff --git a/src/tac2ffi.ml b/src/tac2ffi.ml
index c612cb85a5..19d4259b55 100644
--- a/src/tac2ffi.ml
+++ b/src/tac2ffi.ml
@@ -9,7 +9,6 @@
 open Util
 open Names
 open Globnames
-open Genarg
 open Tac2dyn
 open Tac2expr
 open Proofview.Notations
diff --git a/src/tac2intern.ml b/src/tac2intern.ml
index 0efd9a3005..7b35cd55aa 100644
--- a/src/tac2intern.ml
+++ b/src/tac2intern.ml
@@ -8,7 +8,6 @@
 
 open Pp
 open Util
-open Genarg
 open CErrors
 open Names
 open Libnames
@@ -23,13 +22,8 @@ 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_list = coq_type "list"
 let t_constr = coq_type "constr"
 
-let c_nil = GTacCst (Other t_list, 0, [])
-let c_cons e el = GTacCst (Other t_list, 0, [e; el])
-
 (** Union find *)
 
 module UF :
diff --git a/src/tac2interp.ml b/src/tac2interp.ml
index db30f52772..6f158ac66e 100644
--- a/src/tac2interp.ml
+++ b/src/tac2interp.ml
@@ -9,7 +9,6 @@
 open Util
 open Pp
 open CErrors
-open Genarg
 open Names
 open Proofview.Notations
 open Tac2expr
diff --git a/src/tac2print.ml b/src/tac2print.ml
index 5f34b54ee6..8e4947e332 100644
--- a/src/tac2print.ml
+++ b/src/tac2print.ml
@@ -8,7 +8,6 @@
 
 open Util
 open Pp
-open Genarg
 open Names
 open Tac2expr
 open Tac2env
diff --git a/src/tac2quote.ml b/src/tac2quote.ml
index e89f37f2ba..e967067161 100644
--- a/src/tac2quote.ml
+++ b/src/tac2quote.ml
@@ -40,8 +40,6 @@ let pattern_core n = kername pattern_prefix n
 let global_ref ?loc kn =
   Loc.tag ?loc @@ CTacRef (AbsKn (TacConstant kn))
 
-let dummy_loc = Loc.make_loc (-1, -1)
-
 let constructor ?loc kn args =
   let cst = Loc.tag ?loc @@ CTacCst (AbsKn (Other kn)) in
   if List.is_empty args then cst
diff --git a/src/tac2quote.mli b/src/tac2quote.mli
index b9cae23e63..148e6818dd 100644
--- a/src/tac2quote.mli
+++ b/src/tac2quote.mli
@@ -6,7 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Util
 open Loc
 open Names
 open Tac2dyn
diff --git a/src/tac2stdlib.ml b/src/tac2stdlib.ml
index 2828bbc53f..99fa0370e1 100644
--- a/src/tac2stdlib.ml
+++ b/src/tac2stdlib.ml
@@ -7,12 +7,10 @@
 (************************************************************************)
 
 open Names
-open Globnames
 open Genredexpr
 open Tac2expr
 open Tac2ffi
 open Tac2types
-open Tac2tactics
 open Proofview.Notations
 
 module Value = Tac2ffi
diff --git a/src/tac2tactics.ml b/src/tac2tactics.ml
index 0b25ebb378..b496f5046f 100644
--- a/src/tac2tactics.ml
+++ b/src/tac2tactics.ml
@@ -10,10 +10,8 @@ open Pp
 open Util
 open Names
 open Globnames
-open Misctypes
 open Tac2types
 open Genredexpr
-open Proofview
 open Proofview.Notations
 
 let return = Proofview.tclUNIT
-- 
cgit v1.2.3