Remove some unused values and types

5 files changed, 0 insertions, 44 deletions

diff --git a/checker/closure.ml b/checker/closure.ml
index cef1d31a6..b8294e795 100644
--- a/checker/closure.ml
+++ b/checker/closure.ml
@@ -651,22 +651,6 @@ let drop_parameters depth n argstk =
 
 (** Projections and eta expansion *)
 
-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 *)
-
 let eta_expand_ind_stack env ind m s (f, s') =
   let mib = lookup_mind (fst ind) env in
     match mib.mind_record with
diff --git a/checker/declarations.ml b/checker/declarations.ml
index 56d437c16..ad93146d5 100644
--- a/checker/declarations.ml
+++ b/checker/declarations.ml
@@ -463,13 +463,6 @@ let is_opaque cb = match cb.const_body with
 
 let opaque_univ_context cb = force_lazy_constr_univs cb.const_body
 
-let subst_rel_declaration sub (id,copt,t as x) =
-  let copt' = Option.smartmap (subst_mps sub) copt in
-  let t' = subst_mps sub t in
-  if copt == copt' && t == t' then x else (id,copt',t')
-
-let subst_rel_context sub = List.smartmap (subst_rel_declaration sub)
-
 let subst_recarg sub r = match r with
   | Norec  -> r
   | (Mrec(kn,i)|Imbr (kn,i)) -> let kn' = subst_ind sub kn in
@@ -517,10 +510,6 @@ let subst_decl_arity f g sub ar =
       if x' == x then ar
       else TemplateArity x'
 
-let map_decl_arity f g = function
-  | RegularArity a -> RegularArity (f a)
-  | TemplateArity a -> TemplateArity (g a)
-
 let subst_rel_declaration sub =
   Term.map_rel_decl (subst_mps sub)
 
diff --git a/checker/inductive.ml b/checker/inductive.ml
index ae2f7de8a..8f23a38af 100644
--- a/checker/inductive.ml
+++ b/checker/inductive.ml
@@ -436,13 +436,6 @@ let eq_recarg r1 r2 = match r1, r2 with
 
 let eq_wf_paths = Rtree.equal 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/checker/typeops.ml b/checker/typeops.ml
index 173e19ce1..02d801741 100644
--- a/checker/typeops.ml
+++ b/checker/typeops.ml
@@ -85,9 +85,6 @@ let type_of_constant_knowing_parameters env cst paramtyps =
 let type_of_constant_type env t =
   type_of_constant_type_knowing_parameters env t [||]
 
-let type_of_constant env cst =
-  type_of_constant_knowing_parameters env cst [||]
-
 let judge_of_constant_knowing_parameters env (kn,u as cst) paramstyp =
   let _cb =
     try lookup_constant kn env
diff --git a/checker/univ.ml b/checker/univ.ml
index 668f3a058..fb1a0faa7 100644
--- a/checker/univ.ml
+++ b/checker/univ.ml
@@ -87,7 +87,6 @@ module HList = struct
     val exists : (elt -> bool) -> t -> bool
     val for_all : (elt -> bool) -> t -> bool
     val for_all2 : (elt -> elt -> bool) -> t -> t -> bool
-    val remove : elt -> t -> t
     val to_list : t -> elt list
   end
 
@@ -128,12 +127,6 @@ module HList = struct
   | Nil -> []
   | Cons (x, _, l) -> x :: to_list l
 
-  let rec remove x = function
-  | Nil -> nil
-  | Cons (y, _, l) ->
-    if H.eq x y then l
-    else cons y (remove x l)
-
   end
 end