Remove some unused functions.

Note: they do not even seem to have a debugging purpose, so better remove
them before they bitrot.

4 files changed, 0 insertions, 47 deletions

diff --git a/kernel/declareops.ml b/kernel/declareops.ml
index 73cfd01221..803df78270 100644
--- a/kernel/declareops.ml
+++ b/kernel/declareops.ml
@@ -391,5 +391,3 @@ and hcons_module_body mb =
     mod_delta = delta';
     mod_retroknowledge = retroknowledge';
   }
-
-and hcons_module_type_body mtb = hcons_module_body mtb
diff --git a/kernel/nativevalues.ml b/kernel/nativevalues.ml
index 40bef4bc67..6e097b6133 100644
--- a/kernel/nativevalues.ml
+++ b/kernel/nativevalues.ml
@@ -78,8 +78,6 @@ let accumulate_code (k:accumulator) (x:t) =
 let rec accumulate (x:t) =
   accumulate_code (Obj.magic accumulate) x
 
-let raccumulate = ref accumulate
-
 let mk_accu_gen rcode (a:atom) =
 (*  Format.eprintf "size rcode =%i\n" (Obj.size (Obj.magic rcode)); *)
   let r = Obj.new_block 0 3 in
@@ -160,31 +158,6 @@ let is_accu x =
   let o = Obj.repr x in
   Obj.is_block o && Int.equal (Obj.tag o) accumulate_tag
 
-(*let accumulate_fix_code (k:accumulator) (a:t) =
-  match atom_of_accu k with
-  | Afix(frec,_,rec_pos,_,_) ->
-      let nargs = accu_nargs k in
-      if nargs <> rec_pos || is_accu a then
-	accumulate_code k a
-      else
-        let r = ref frec in
-        for i = 0 to nargs - 1 do
-	  r := !r (arg_of_accu k i)
-        done;
-        !r a
-  | _ -> assert false
-
-
-let rec accumulate_fix (x:t) =
-  accumulate_fix_code (Obj.magic accumulate_fix) x
-
-let raccumulate_fix = ref accumulate_fix *)
-
-let is_atom_fix (a:atom) =
-  match a with
-  | Afix _ -> true
-  | _ -> false
-
 let mk_fix_accu rec_pos pos types bodies =
   mk_accu_gen accumulate (Afix(types,bodies,rec_pos, pos))
 
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index c7ab6491d7..33aa2972b2 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -222,13 +222,6 @@ let inline_private_constants_in_constr = Term_typing.inline_side_effects
 let inline_private_constants_in_definition_entry = Term_typing.inline_entry_side_effects
 let side_effects_of_private_constants x = Term_typing.uniq_seff (List.rev x)
 
-let constant_entry_of_private_constant = function
-  | { Entries.eff = Entries.SEsubproof (kn, cb, eff_env) } ->
-      [ kn, Term_typing.constant_entry_of_side_effect cb eff_env ]
-  | { Entries.eff = Entries.SEscheme (l,_) } ->
-      List.map (fun (_,kn,cb,eff_env) ->
-        kn, Term_typing.constant_entry_of_side_effect cb eff_env) l
-
 let private_con_of_con env c =
   let cbo = Environ.lookup_constant c env.env in
   { Entries.from_env = Ephemeron.create env.revstruct;
diff --git a/kernel/term.ml b/kernel/term.ml
index 455248dd52..2060c7b6e9 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -486,8 +486,6 @@ let lambda_applist c l =
 
 let lambda_appvect c v = lambda_applist c (Array.to_list v)
 
-let lambda_app c a = lambda_applist c [a]
-
 let lambda_applist_assum n c l =
   let rec app n subst t l =
     if Int.equal n 0 then
@@ -501,15 +499,6 @@ let lambda_applist_assum n c l =
 
 let lambda_appvect_assum n c v = lambda_applist_assum n c (Array.to_list v)
 
-(* pseudo-reduction rule:
- * [prod_app  s (Prod(_,B)) N --> B[N]
- * with an strip_outer_cast on the first argument to produce a product *)
-
-let prod_app t n =
-  match kind_of_term (strip_outer_cast t) with
-    | Prod (_,_,b) -> subst1 n b
-    | _ -> anomaly (str"Needed a product, but didn't find one")
-
 (* prod_applist T [ a1 ; ... ; an ] -> (T a1 ... an) *)
 let prod_applist c l =
   let rec app subst c l =