Merge PR#582: Fix warnings

7 files changed, 2 insertions, 36 deletions

diff --git a/engine/eConstr.ml b/engine/eConstr.ml
index bb9075e74a..54d3ce6cf7 100644
--- a/engine/eConstr.ml
+++ b/engine/eConstr.ml
@@ -6,7 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open CSig
 open CErrors
 open Util
 open Names
diff --git a/engine/eConstr.mli b/engine/eConstr.mli
index 3a9469e55a..693b592fd4 100644
--- a/engine/eConstr.mli
+++ b/engine/eConstr.mli
@@ -9,7 +9,6 @@
 open CSig
 open Names
 open Constr
-open Context
 open Environ
 
 type t
diff --git a/engine/evarutil.ml b/engine/evarutil.ml
index 22f93faa6f..e85c1f6fd8 100644
--- a/engine/evarutil.ml
+++ b/engine/evarutil.ml
@@ -10,7 +10,6 @@ open CErrors
 open Util
 open Names
 open Term
-open Vars
 open Termops
 open Namegen
 open Pre_env
diff --git a/engine/evd.ml b/engine/evd.ml
index 5419a10a8e..db048bbd6e 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -14,10 +14,8 @@ open Nameops
 open Term
 open Vars
 open Environ
-open Globnames
-open Context.Named.Declaration
 
-module RelDecl = Context.Rel.Declaration
+(* module RelDecl = Context.Rel.Declaration *)
 module NamedDecl = Context.Named.Declaration
 
 (** Generic filters *)
@@ -360,8 +358,6 @@ module EvMap = Evar.Map
 module EvNames :
 sig
 
-open Misctypes
-
 type t
 
 val empty : t
diff --git a/engine/proofview.mli b/engine/proofview.mli
index a3b0304b17..da8a8fecdd 100644
--- a/engine/proofview.mli
+++ b/engine/proofview.mli
@@ -13,7 +13,6 @@
     state and returning a value of type ['a]. *)
 
 open Util
-open Term
 open EConstr
 
 (** Main state of tactics *)
diff --git a/engine/termops.ml b/engine/termops.ml
index 64f4c6dc5e..19e62f8e62 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -612,30 +612,6 @@ let adjust_app_array_size f1 l1 f2 l2 =
     let extras,restl1 = Array.chop (len1-len2) l1 in
     (mkApp (f1,extras), restl1, f2, l2)
 
-(* [map_constr_with_named_binders g f l c] maps [f l] on the immediate
-   subterms of [c]; it carries an extra data [l] (typically a name
-   list) which is processed by [g na] (which typically cons [na] to
-   [l]) at each binder traversal (with name [na]); it is not recursive
-   and the order with which subterms are processed is not specified *)
-
-let map_constr_with_named_binders g f l c = match kind_of_term c with
-  | (Rel _ | Meta _ | Var _   | Sort _ | Const _ | Ind _
-    | Construct _) -> c
-  | Cast (c,k,t) -> mkCast (f l c, k, f l t)
-  | Prod (na,t,c) -> mkProd (na, f l t, f (g na l) c)
-  | Lambda (na,t,c) -> mkLambda (na, f l t, f (g na l) c)
-  | LetIn (na,b,t,c) -> mkLetIn (na, f l b, f l t, f (g na l) c)
-  | App (c,al) -> mkApp (f l c, Array.map (f l) al)
-  | Proj (p,c) -> mkProj (p, f l c)
-  | Evar (e,al) -> mkEvar (e, Array.map (f l) al)
-  | Case (ci,p,c,bl) -> mkCase (ci, f l p, f l c, Array.map (f l) bl)
-  | Fix (ln,(lna,tl,bl)) ->
-      let l' = Array.fold_left (fun l na -> g na l) l lna in
-      mkFix (ln,(lna,Array.map (f l) tl,Array.map (f l') bl))
-  | CoFix(ln,(lna,tl,bl)) ->
-      let l' = Array.fold_left (fun l na -> g na l) l lna in
-      mkCoFix (ln,(lna,Array.map (f l) tl,Array.map (f l') bl))
-
 (* [map_constr_with_binders_left_to_right g f n c] maps [f n] on the
    immediate subterms of [c]; it carries an extra data [n] (typically
    a lift index) which is processed by [g] (which typically add 1 to
@@ -1451,7 +1427,6 @@ let dependency_closure env sigma sign hyps =
     List.rev lh
 
 let global_app_of_constr sigma c =
-  let open Univ in
   let open Globnames in
   match EConstr.kind sigma c with
   | Const (c, u) -> (ConstRef c, u), None
diff --git a/engine/universes.ml b/engine/universes.ml
index ad5ff827bd..1900112dde 100644
--- a/engine/universes.ml
+++ b/engine/universes.ml
@@ -13,7 +13,6 @@ open Term
 open Environ
 open Univ
 open Globnames
-open Decl_kinds
 
 let pr_with_global_universes l = 
   try Nameops.pr_id (LMap.find l (snd (Global.global_universe_names ())))
@@ -732,7 +731,7 @@ let instantiate_with_lbound u lbound lower alg enforce (ctx, us, algs, insts, cs
 
 type constraints_map = (Univ.constraint_type * Univ.LMap.key) list Univ.LMap.t
 
-let pr_constraints_map cmap =
+let _pr_constraints_map (cmap:constraints_map) =
   LMap.fold (fun l cstrs acc -> 
     Level.pr l ++ str " => " ++ 
       prlist_with_sep spc (fun (d,r) -> pr_constraint_type d ++ Level.pr r) cstrs ++