still some more dead code removal

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15875 85f007b7-540e-0410-9357-904b9bb8a0f7

11 files changed, 4 insertions, 20 deletions

diff --git a/checker/check_stat.ml b/checker/check_stat.ml
index 0e7aec1a8..3176a4307 100644
--- a/checker/check_stat.ml
+++ b/checker/check_stat.ml
@@ -7,12 +7,7 @@
 (************************************************************************)
 
 open Pp
-open Errors
-open Util
-open System
-open Flags
 open Names
-open Term
 open Declarations
 open Environ
 
diff --git a/checker/checker.ml b/checker/checker.ml
index ea2e3892f..8389803fc 100644
--- a/checker/checker.ml
+++ b/checker/checker.ml
@@ -12,7 +12,6 @@ open Util
 open System
 open Flags
 open Names
-open Term
 open Check
 
 let () = at_exit flush_all
diff --git a/checker/closure.ml b/checker/closure.ml
index f86aa82eb..c515bdb24 100644
--- a/checker/closure.ml
+++ b/checker/closure.ml
@@ -6,7 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Errors
 open Util
 open Pp
 open Term
diff --git a/checker/declarations.ml b/checker/declarations.ml
index 8b146d18b..df0134e02 100644
--- a/checker/declarations.ml
+++ b/checker/declarations.ml
@@ -1,4 +1,3 @@
-open Errors
 open Util
 open Names
 open Term
@@ -111,7 +110,7 @@ let map_mp mp1 mp2 = add_mp mp1 mp2 empty_subst
 let mp_in_delta mp =
   Deltamap.mem_mp mp
 
-let rec find_prefix resolve mp =
+let find_prefix resolve mp =
   let rec sub_mp = function
     | MPdot(mp,l) as mp_sup ->
 	(try Deltamap.find_mp mp_sup resolve
diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml
index a51b66ce0..7dfa29e16 100644
--- a/checker/mod_checking.ml
+++ b/checker/mod_checking.ml
@@ -4,7 +4,6 @@ open Errors
 open Util
 open Names
 open Term
-open Inductive
 open Reduction
 open Typeops
 open Indtypes
diff --git a/checker/modops.ml b/checker/modops.ml
index 9d5829605..1c4a2916e 100644
--- a/checker/modops.ml
+++ b/checker/modops.ml
@@ -11,10 +11,8 @@ open Errors
 open Util
 open Pp
 open Names
-open Univ
 open Term
 open Declarations
-open Environ
 (*i*)
 
 let error_not_a_constant l =
diff --git a/checker/reduction.ml b/checker/reduction.ml
index 195f7d423..c2d5c261c 100644
--- a/checker/reduction.ml
+++ b/checker/reduction.ml
@@ -8,7 +8,6 @@
 
 open Errors
 open Util
-open Names
 open Term
 open Univ
 open Closure
diff --git a/checker/subtyping.ml b/checker/subtyping.ml
index 7d2ced7fd..390c2b9e7 100644
--- a/checker/subtyping.ml
+++ b/checker/subtyping.ml
@@ -18,9 +18,6 @@ open Reduction
 open Inductive
 open Modops
 (*i*)
-open Pp
-
-
 
 (* This local type is used to subtype a constant with a constructor or
    an inductive type. It can also be useful to allow reorderings in
diff --git a/checker/term.ml b/checker/term.ml
index b41bebca2..0c3fc741d 100644
--- a/checker/term.ml
+++ b/checker/term.ml
@@ -10,7 +10,6 @@
 
 open Errors
 open Util
-open Pp
 open Names
 open Univ
 open Esubst
@@ -134,7 +133,7 @@ let rec strip_outer_cast c = match c with
   | Cast (c,_,_) -> strip_outer_cast c
   | _ -> c
 
-let rec collapse_appl c = match c with
+let collapse_appl c = match c with
   | App (f,cl) ->
       let rec collapse_rec f cl2 =
         match (strip_outer_cast f) with
diff --git a/checker/typeops.ml b/checker/typeops.ml
index 91f58a04a..ad05f96b7 100644
--- a/checker/typeops.ml
+++ b/checker/typeops.ml
@@ -75,7 +75,7 @@ let judge_of_variable env id =
 (* Checks if a context of variable can be instantiated by the
    variables of the current env *)
 (* TODO: check order? *)
-let rec check_hyps_inclusion env sign =
+let check_hyps_inclusion env sign =
   fold_named_context
     (fun (id,_,ty1) () ->
       let ty2 = named_type id env in
diff --git a/checker/validate.ml b/checker/validate.ml
index 2f46695cd..eeff9d1cd 100644
--- a/checker/validate.ml
+++ b/checker/validate.ml
@@ -164,7 +164,7 @@ let val_set ?(name="Set.t") f =
 		     vset;ext "bal" val_int|]|])
 
 (* Maps *)
-let rec val_map ?(name="Map.t") fk fv =
+let val_map ?(name="Map.t") fk fv =
   val_rec_sum name 1
     (fun vmap ->
        [|[|vmap; ext "key" fk; ext "value" fv;