From f461e7657cab9917c5b405427ddba3d56f197efb Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 8 May 2016 18:59:55 +0200
Subject: Removing dead code and unused opens.

---
 pretyping/evardefine.ml  | 2 --
 pretyping/evarsolve.ml   | 1 -
 pretyping/nativenorm.ml  | 1 -
 pretyping/typeclasses.ml | 2 +-
 4 files changed, 1 insertion(+), 5 deletions(-)

(limited to 'pretyping')

diff --git a/pretyping/evardefine.ml b/pretyping/evardefine.ml
index ef3a3f5255..d349cf8216 100644
--- a/pretyping/evardefine.ml
+++ b/pretyping/evardefine.ml
@@ -6,7 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Errors
 open Util
 open Pp
 open Names
@@ -14,7 +13,6 @@ open Term
 open Vars
 open Termops
 open Namegen
-open Pre_env
 open Environ
 open Evd
 open Evarutil
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index 3d1822102a..455a7dbd69 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -20,7 +20,6 @@ open Reductionops
 open Evarutil
 open Pretype_errors
 open Sigma.Notations
-open Context.Rel.Declaration
 
 let normalize_evar evd ev =
   match kind_of_term (whd_evar evd (mkEvar ev)) with
diff --git a/pretyping/nativenorm.ml b/pretyping/nativenorm.ml
index 8ddfeaf2f0..17bf28793f 100644
--- a/pretyping/nativenorm.ml
+++ b/pretyping/nativenorm.ml
@@ -18,7 +18,6 @@ open Inductive
 open Util
 open Nativecode
 open Nativevalues
-open Nativelambda
 open Context.Rel.Declaration
 
 (** This module implements normalization by evaluation to OCaml code *)
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index 3a5796fe1b..3ff96cd72a 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -25,7 +25,7 @@ let get_typeclasses_unique_solutions () = !typeclasses_unique_solutions
 
 open Goptions
 
-let set_typeclasses_unique_solutions =
+let _ =
   declare_bool_option
     { optsync  = true;
       optdepr  = false;
-- 
cgit v1.2.3