Removing dead code.

16 files changed, 0 insertions, 55 deletions

diff --git a/kernel/cbytegen.mli b/kernel/cbytegen.mli
index eab36d8b2..8fb6601a9 100644
--- a/kernel/cbytegen.mli
+++ b/kernel/cbytegen.mli
@@ -1,4 +1,3 @@
-open Names
 open Cbytecodes
 open Cemitcodes
 open Term
diff --git a/kernel/cemitcodes.ml b/kernel/cemitcodes.ml
index 3c9692a5c..9ecae2b36 100644
--- a/kernel/cemitcodes.ml
+++ b/kernel/cemitcodes.ml
@@ -10,7 +10,6 @@
    machine, Oct 2004 *)
 (* Extension: Arnaud Spiwack (support for native arithmetic), May 2005 *)
 
-open Names
 open Term
 open Cbytecodes
 open Copcodes
diff --git a/kernel/closure.ml b/kernel/closure.ml
index f06b13d8d..6824c399e 100644
--- a/kernel/closure.ml
+++ b/kernel/closure.ml
@@ -771,24 +771,6 @@ let drop_parameters depth n argstk =
   (* we know that n < stack_args_size(argstk) (if well-typed term) *) 
   anomaly (Pp.str "ill-typed term: found a match on a partially applied constructor")
 
-
-let rec get_parameters depth n argstk =
-  match argstk with
-      Zapp args::s ->
-        let q = Array.length args in
-        if n > q then Array.append args (get_parameters depth (n-q) s)
-        else if Int.equal n q then [||]
-        else Array.sub args 0 n
-    | Zshift(k)::s -> 
-      get_parameters (depth-k) n s
-    | [] -> (* we know that n < stack_args_size(argstk) (if well-typed term) *)
-	if Int.equal n 0 then [||]
-	else raise Not_found (* Trying to eta-expand a partial application..., should do 
-				eta expansion first? *)
-    | _ -> assert false
-	(* strip_update_shift_app only produces Zapp and Zshift items *)
-
-
 (** [eta_expand_ind_stack env ind c s t] computes stacks correspoding 
     to the conversion of the eta expansion of t, considered as an inhabitant 
     of ind, and the Constructor c of this inductive type applied to arguments
diff --git a/kernel/declareops.mli b/kernel/declareops.mli
index 47a82cc6c..ce65af975 100644
--- a/kernel/declareops.mli
+++ b/kernel/declareops.mli
@@ -9,7 +9,6 @@
 open Declarations
 open Mod_subst
 open Univ
-open Context
 
 (** Operations concerning types in [Declarations] :
     [constant_body], [mutual_inductive_body], [module_body] ... *)
diff --git a/kernel/fast_typeops.mli b/kernel/fast_typeops.mli
index 4c2c92ccf..90d9c55f1 100644
--- a/kernel/fast_typeops.mli
+++ b/kernel/fast_typeops.mli
@@ -6,13 +6,8 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Names
-open Univ
 open Term
-open Context
 open Environ
-open Entries
-open Declarations
 
 (** {6 Typing functions (not yet tagged as safe) }
     
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 99d9f52c9..ea575e1e0 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -654,7 +654,6 @@ let used_section_variables env inds =
   keep_hyps env ids
 
 let rel_vect n m = Array.init m (fun i -> mkRel(n+m-i))
-let rel_appvect n m = rel_vect n (List.length m)
 
 exception UndefinableExpansion
 
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index bb57ad256..6b4dd536a 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -447,13 +447,6 @@ type subterm_spec =
 
 let eq_wf_paths = Rtree.equal Declareops.eq_recarg
 
-let pp_recarg = function
-  | Norec -> Pp.str "Norec"
-  | Mrec i -> Pp.str ("Mrec "^MutInd.to_string (fst i))
-  | Imbr i -> Pp.str ("Imbr "^MutInd.to_string (fst i))
-
-let pp_wf_paths = Rtree.pp_tree pp_recarg
-
 let inter_recarg r1 r2 = match r1, r2 with
 | Norec, Norec -> Some r1
 | Mrec i1, Mrec i2
diff --git a/kernel/names.ml b/kernel/names.ml
index b349ccb00..4ccf5b60a 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -571,7 +571,6 @@ let constr_modpath (ind,_) = ind_modpath ind
 
 let ith_mutual_inductive (mind, _) i = (mind, i)
 let ith_constructor_of_inductive ind i = (ind, i)
-let ith_constructor_of_pinductive (ind,u) i = ((ind,i),u)
 let inductive_of_constructor (ind, i) = ind
 let index_of_constructor (ind, i) = i
 
diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml
index 1a4a4b54d..ada7ae737 100644
--- a/kernel/nativecode.ml
+++ b/kernel/nativecode.ml
@@ -12,7 +12,6 @@ open Context
 open Declarations
 open Util
 open Nativevalues
-open Primitives
 open Nativeinstr
 open Nativelambda
 open Pre_env
diff --git a/kernel/nativelambda.mli b/kernel/nativelambda.mli
index 6a97edc40..ccf2888b5 100644
--- a/kernel/nativelambda.mli
+++ b/kernel/nativelambda.mli
@@ -8,7 +8,6 @@
 open Names
 open Term
 open Pre_env
-open Nativevalues
 open Nativeinstr
 
 (** This file defines the lambda code generation phase of the native compiler *)
diff --git a/kernel/nativelibrary.ml b/kernel/nativelibrary.ml
index 914f577e2..0b8662ff0 100644
--- a/kernel/nativelibrary.ml
+++ b/kernel/nativelibrary.ml
@@ -12,7 +12,6 @@ open Environ
 open Mod_subst
 open Modops
 open Nativecode
-open Nativelib
 
 (** This file implements separate compilation for libraries in the native
 compiler *)
diff --git a/kernel/opaqueproof.mli b/kernel/opaqueproof.mli
index 87cebd62f..0609c8517 100644
--- a/kernel/opaqueproof.mli
+++ b/kernel/opaqueproof.mli
@@ -9,7 +9,6 @@
 open Names
 open Term
 open Mod_subst
-open Int
 
 (** This module implements the handling of opaque proof terms.
     Opauqe proof terms are special since:
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 4153b323b..b09367dd9 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -28,14 +28,6 @@ open Esubst
 
 let left2right = ref false
 
-let conv_key k =
-  match k with
-    VarKey id -> 
-    VarKey id
-  | ConstKey (cst,_) -> 
-     ConstKey cst
-  | RelKey n -> RelKey n
-		       
 let rec is_empty_stack = function
   [] -> true
   | Zupdate _::s -> is_empty_stack s
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index a3441aa3e..b54511e40 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -15,7 +15,6 @@
 open Errors
 open Util
 open Names
-open Univ
 open Term
 open Context
 open Declarations
@@ -101,10 +100,6 @@ let hcons_j j =
 
 let feedback_completion_typecheck =
   Option.iter (fun state_id -> Pp.feedback ~state_id Feedback.Complete)
-  
-let subst_instance_j s j =
-  { uj_val = Vars.subst_univs_level_constr s j.uj_val;
-    uj_type = Vars.subst_univs_level_constr s j.uj_type }
 
 let infer_declaration env kn dcl =
   match dcl with
diff --git a/kernel/term_typing.mli b/kernel/term_typing.mli
index 696fc3d2d..1b54b1ea1 100644
--- a/kernel/term_typing.mli
+++ b/kernel/term_typing.mli
@@ -8,7 +8,6 @@
 
 open Names
 open Term
-open Univ
 open Environ
 open Declarations
 open Entries
diff --git a/kernel/vconv.ml b/kernel/vconv.ml
index 80b15f8ba..29315b0a9 100644
--- a/kernel/vconv.ml
+++ b/kernel/vconv.ml
@@ -42,8 +42,6 @@ let conv_vect fconv vect1 vect2 cu =
 
 let infos = ref (create_clos_infos betaiotazeta Environ.empty_env)
 
-let eq_table_key = Names.eq_table_key eq_constant
-
 let rec conv_val env pb k v1 v2 cu =
   if v1 == v2 then cu
   else conv_whd env pb k (whd_val v1) (whd_val v2) cu