Merge PR#582: Fix warnings

9 files changed, 1 insertions, 21 deletions

diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index f9ebc42330..605914a015 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -27,11 +27,6 @@ open Unification
 open Misctypes
 open Sigma.Notations
 
-(* Abbreviations *)
-
-let pf_env = Refiner.pf_env
-let pf_type_of gls c  = Typing.unsafe_type_of (pf_env gls) gls.sigma c
-
 (******************************************************************)
 (* Clausal environments *)
 
diff --git a/proofs/clenvtac.mli b/proofs/clenvtac.mli
index 5b7164705a..26069207eb 100644
--- a/proofs/clenvtac.mli
+++ b/proofs/clenvtac.mli
@@ -8,7 +8,6 @@
 
 (** Legacy components of the previous proof engine. *)
 
-open Term
 open Clenv
 open EConstr
 open Unification
diff --git a/proofs/goal.ml b/proofs/goal.ml
index 9046f45341..fc8e635a07 100644
--- a/proofs/goal.ml
+++ b/proofs/goal.ml
@@ -8,7 +8,6 @@
 
 open Util
 open Pp
-open Term
 open Sigma.Notations
 
 module NamedDecl = Context.Named.Declaration
diff --git a/proofs/logic.ml b/proofs/logic.ml
index e6024785db..9ab8c34d89 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -97,11 +97,6 @@ let check_typability env sigma c =
    (instead of iterating on the list of identifier to be removed, which
    forces the user to give them in order). *)
 
-let clear_hyps env sigma ids sign cl =
-  let evdref = ref (Evd.clear_metas sigma) in
-  let (hyps,cl) = Evarutil.clear_hyps_in_evi env evdref sign cl ids in
-  (hyps, cl, !evdref)
-
 let clear_hyps2 env sigma ids sign t cl =
   let evdref = ref (Evd.clear_metas sigma) in
   let (hyps,t,cl) = Evarutil.clear_hyps2_in_evi env evdref sign t cl ids in
diff --git a/proofs/proof_type.mli b/proofs/proof_type.mli
index 03bc5e4710..e59db9e427 100644
--- a/proofs/proof_type.mli
+++ b/proofs/proof_type.mli
@@ -11,9 +11,6 @@
 open Evd
 open Names
 open Term
-open Glob_term
-open Nametab
-open Misctypes
 
 (** This module defines the structure of proof tree and the tactic type. So, it
    is used by [Proof_tree] and [Refiner] *)
diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml
index 0fe5c73f15..cb35384227 100644
--- a/proofs/redexpr.ml
+++ b/proofs/redexpr.ml
@@ -43,7 +43,7 @@ let cbv_native env sigma c =
 
 let whd_cbn flags env sigma t =
   let (state,_) =
-    (whd_state_gen true true flags env sigma (t,Reductionops.Stack.empty))
+    (whd_state_gen ~refold:true ~tactic_mode:true flags env sigma (t,Reductionops.Stack.empty))
   in
   Reductionops.Stack.zip ~refold:true sigma state
 
diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index bc12b3ba71..259e96a276 100644
--- a/proofs/refiner.ml
+++ b/proofs/refiner.ml
@@ -10,7 +10,6 @@ open Pp
 open CErrors
 open Util
 open Evd
-open Environ
 open Proof_type
 open Logic
 
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index b55f8ef113..97c5cda770 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -179,9 +179,6 @@ module New = struct
   let pf_unsafe_type_of gl t =
     pf_apply unsafe_type_of gl t
 
-  let pf_get_type_of gl t =
-    pf_apply (Retyping.get_type_of ~lax:true) gl t
-
   let pf_type_of gl t =
     pf_apply type_of gl t
 
diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli
index 627a8e0e7e..e6e60e27f7 100644
--- a/proofs/tacmach.mli
+++ b/proofs/tacmach.mli
@@ -15,7 +15,6 @@ open Proof_type
 open Redexpr
 open Pattern
 open Locus
-open Misctypes
 
 (** Operations for handling terms under a local typing context. *)