Removing dead code.

8 files changed, 2 insertions, 120 deletions

diff --git a/kernel/constr.ml b/kernel/constr.ml
index 9be04c765..b2aa5690b 100644
--- a/kernel/constr.ml
+++ b/kernel/constr.ml
@@ -143,7 +143,6 @@ let mkApp (f, a) =
       | App (g, cl) -> App (g, Array.append cl a)
       | _ -> App (f, a)
 
-let out_punivs (a, _) = a
 let map_puniverses f (x,u) = (f x, u)
 let in_punivs a = (a, Univ.Instance.empty)
 
@@ -547,9 +546,6 @@ let compare_head_gen_leq eq_universes eq_sorts leq_sorts eq leq t1 t2 =
 let rec eq_constr m n =
   (m == n) || compare_head_gen (fun _ -> Instance.equal) Sorts.equal eq_constr m n
 
-(** Strict equality of universe instances. *)
-let compare_constr = compare_head_gen (fun _ -> Instance.equal) Sorts.equal
-
 let equal m n = eq_constr m n (* to avoid tracing a recursive fun *)
 
 let eq_constr_univs univs m n =
@@ -989,7 +985,7 @@ module Hsorts =
 	| Type u -> 2 + Universe.hash u
     end)
 
-let hcons_sorts = Hashcons.simple_hcons Hsorts.generate hcons_univ
+(* let hcons_sorts = Hashcons.simple_hcons Hsorts.generate hcons_univ *)
 let hcons_caseinfo = Hashcons.simple_hcons Hcaseinfo.generate hcons_ind
 
 let hcons =
diff --git a/kernel/environ.ml b/kernel/environ.ml
index 5bd0edf69..48a7964c3 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -220,10 +220,6 @@ let universes_and_subst_of cb u =
   let subst = Univ.make_universe_subst u univs in
     subst, Univ.instantiate_univ_context subst univs
 
-let get_regular_arity = function
-  | RegularArity a -> a
-  | TemplateArity _ -> assert false
-
 let map_regular_arity f = function
   | RegularArity a as ar -> 
     let a' = f a in 
@@ -374,8 +370,6 @@ let add_mind kn mib env =
 
 (* Lookup of section variables *)
 
-let constant_body_hyps cb = cb.const_hyps
-
 let lookup_constant_variables c env =
   let cmap = lookup_constant c env in
   Context.vars_of_named_context cmap.const_hyps
diff --git a/kernel/fast_typeops.ml b/kernel/fast_typeops.ml
index 94e4479d2..83f1e74ba 100644
--- a/kernel/fast_typeops.ml
+++ b/kernel/fast_typeops.ml
@@ -12,10 +12,8 @@ open Names
 open Univ
 open Term
 open Vars
-open Context
 open Declarations
 open Environ
-open Entries
 open Reduction
 open Inductive
 open Type_errors
@@ -62,7 +60,6 @@ let assumption_of_judgment env t ty =
 (* Prop and Set *)
 
 let judge_of_prop = mkSort type1_sort
-let judge_of_set = judge_of_prop
 
 let judge_of_prop_contents _ = judge_of_prop
 
@@ -122,16 +119,6 @@ let type_of_constant_knowing_parameters env cst paramtyps =
   let ty, cu = constant_type env cst in
     type_of_constant_knowing_parameters_arity env ty paramtyps, cu
 
-let type_of_constant_type env t =
-  type_of_constant_knowing_parameters_arity env t [||]
-
-let type_of_constant env cst =
-  type_of_constant_knowing_parameters env cst [||]
-
-let type_of_constant_in env cst =
-  let ar = constant_type_in env cst in
-    type_of_constant_knowing_parameters_arity env ar [||]
-
 let judge_of_constant_knowing_parameters env (kn,u as cst) args =
   let cb = lookup_constant kn env in
   let () = check_hyps_inclusion env mkConstU cst cb.const_hyps in
@@ -142,18 +129,6 @@ let judge_of_constant_knowing_parameters env (kn,u as cst) args =
 let judge_of_constant env cst =
   judge_of_constant_knowing_parameters env cst [||]
 
-let type_of_projection env (cst,u) =
-  let cb = lookup_constant cst env in
-  match cb.const_proj with
-  | Some pb -> 
-    if cb.const_polymorphic then
-      let mib,_ = lookup_mind_specif env (pb.proj_ind,0) in
-      let subst = make_inductive_subst mib u in
-	Vars.subst_univs_level_constr subst pb.proj_type
-    else pb.proj_type
-  | None -> raise (Invalid_argument "type_of_projection: not a projection")
-
-
 (* Type of a lambda-abstraction. *)
 
 (* [judge_of_abstraction env name var j] implements the rule
@@ -169,11 +144,6 @@ let type_of_projection env (cst,u) =
 let judge_of_abstraction env name var ty =
   mkProd (name, var, ty)
 
-(* Type of let-in. *)
-
-let judge_of_letin env name defj typj j =
-  subst1 defj j
-
 (* Type of an application. *)
 
 let make_judgev c t = 
@@ -490,26 +460,3 @@ let infer_type env constr =
 let infer_v env cv =
   let jv = execute_array env cv in
     make_judgev cv jv
-
-(* Typing of several terms. *)
-
-let infer_local_decl env id = function
-  | LocalDef c ->
-      let t = execute env c in
-      (Name id, Some c, t)
-  | LocalAssum c ->
-      let t = execute env c in
-      (Name id, None, assumption_of_judgment env c t)
-
-let infer_local_decls env decls =
-  let rec inferec env = function
-  | (id, d) :: l ->
-      let (env, l) = inferec env l in
-      let d = infer_local_decl env id d in
-	(push_rel d env, add_rel_decl d l)
-  | [] -> (env, empty_rel_context) in
-  inferec env decls
-
-(* Exported typing functions *)
-
-let typing env c = infer env c
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 85d04e5e2..014bfba29 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -102,14 +102,6 @@ let mind_check_names mie =
 
 (* Typing the arities and constructor types *)
 
-let is_logic_type t = is_prop_sort t.utj_type
-
-(* [infos] is a sequence of pair [islogic,issmall] for each type in
-   the product of a constructor or arity *)
-
-let is_small infos = List.for_all (fun (logic,small) -> small) infos
-let is_logic_constr infos = List.for_all (fun (logic,small) -> logic) infos
-
 (* An inductive definition is a "unit" if it has only one constructor
    and that all arguments expected by this constructor are
    logical, this is the case for equality, conjunction of logical properties
@@ -153,23 +145,9 @@ let infos_and_sort env ctx t =
    w1,w2,w3 <= u3
 *)
 
-let extract_level (_,_,lc,(_,lev)) =
-  (* Enforce that the level is not in Prop if more than one constructor *)
-  (* if Array.length lc >= 2 then sup type0_univ lev else lev *)
-  lev
-
-let inductive_levels arities inds =
-  let cstrs_levels = Array.map extract_level inds in
-  (* Take the transitive closure of the system of constructors *)
-  (* level constraints and remove the recursive dependencies *)
-    cstrs_levels
-
 (* This (re)computes informations relevant to extraction and the sort of an
    arity or type constructor; we do not to recompute universes constraints *)
 
-let context_set_list_union =
-  List.fold_left ContextSet.union ContextSet.empty
-
 let infer_constructor_packet env_ar_par ctx params lc =
   (* type-check the constructors *)
   let jlc = List.map (infer_type env_ar_par) lc in
@@ -691,11 +669,7 @@ let used_section_variables env inds =
       Id.Set.empty inds in
   keep_hyps env ids
 
-let lift_decl n d = 
-  map_rel_declaration (lift n) d
-
 let rel_vect n m = Array.init m (fun i -> mkRel(n+m-i))
-let rel_list n m = Array.to_list (rel_vect n m)
 let rel_appvect n m = rel_vect n (List.length m)
 
 exception UndefinableExpansion
@@ -707,7 +681,7 @@ exception UndefinableExpansion
 let compute_expansion ((kn, _ as ind), u) params ctx =
   let mp, dp, l = repr_mind kn in
   let make_proj id = Constant.make1 (KerName.make mp dp (Label.of_id id)) in
-  let rec projections acc (na, b, t) =
+  let projections acc (na, b, t) =
     match b with
     | Some c -> acc
     | None -> 
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index f07217ac0..64b2c76f9 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -19,9 +19,6 @@ open Environ
 open Reduction
 open Type_errors
 
-type pinductive = inductive puniverses
-type pconstructor = constructor puniverses
-
 type mind_specif = mutual_inductive_body * one_inductive_body
 
 (* raise Not_found if not an inductive type *)
@@ -157,10 +154,6 @@ let sort_as_univ = function
 let cons_subst u su subst =
   Univ.LMap.add u su subst
 
-let actualize_decl_level env lev t =
-  let sign,s = dest_arity env t in
-  mkArity (sign,lev)
-
 (* Bind expected levels of parameters to actual levels *)
 (* Propagate the new levels in the signature *)
 let rec make_subst env = function
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index a6e107d3f..1e6f157ab 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -172,7 +172,6 @@ type conv_pb =
   | CUMUL
 
 let is_cumul = function CUMUL -> true | CONV -> false
-let is_pos = function Pos -> true | Null -> false
 
 type 'a universe_compare = 
   { (* Might raise NotConvertible *)
@@ -186,8 +185,6 @@ type ('a,'b) generic_conversion_function = env -> 'b universe_state -> 'a -> 'a
 
 type 'a infer_conversion_function = env -> Univ.universes -> 'a -> 'a -> Univ.constraints
 
-type conv_universes = Univ.universes * Univ.constraints option
-
 let sort_cmp_universes pb s0 s1 (u, check) =
   (check.compare pb s0 s1 u, check)
 
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 3e11ede0e..0578d35fc 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -802,12 +802,6 @@ let register field value by_clause senv =
       Retroknowledge.RKRegister (field,value)::senv.local_retroknowledge
   }
 
-(* spiwack : currently unused *)
-let unregister field senv =
-  (*spiwack: todo: do things properly or delete *)
-  { senv with env = Environ.unregister senv.env field}
-(* /spiwack *)
-
 (* This function serves only for inlining constants in native compiler for now,
 but it is meant to become a replacement for environ.register *)
 let register_inline kn senv =
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index 147fe8a9d..437f7b832 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -24,10 +24,6 @@ open Entries
 open Typeops
 open Fast_typeops
 
-let debug = true
-let prerr_endline =
-  if debug then prerr_endline else fun _ -> ()
-
 let constrain_type env j poly = function
   | `None -> 
     if not poly then (* Old-style polymorphism *)
@@ -46,15 +42,6 @@ let constrain_type env j poly = function
 
 let map_option_typ = function None -> `None | Some x -> `Some x
 
-let local_constrain_type env j = function
-  | None ->
-      j.uj_type
-  | Some t ->
-      let tj = infer_type env t in
-      let _ = judge_of_cast env j DEFAULTcast tj in
-      assert (eq_constr t tj.utj_val);
-      t
-
 (* Insertion of constants and parameters in environment. *)
 
 let mk_pure_proof c = (c, Univ.ContextSet.empty), Declareops.no_seff