From 80bbdf335be5657f5ab33b4aa02e21420d341de2 Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond <guillaume.melquiond@inria.fr>
Date: Sat, 2 Jan 2016 17:11:03 +0100
Subject: Remove some unused functions.

Note: they do not even seem to have a debugging purpose, so better remove
them before they bitrot.
---
 engine/proofview_monad.ml |  5 -----
 ide/coq.ml                |  5 -----
 ide/document.ml           |  6 ------
 ide/wg_ProofView.ml       | 13 -------------
 interp/constrextern.ml    |  9 ---------
 interp/constrintern.ml    | 13 -------------
 kernel/declareops.ml      |  2 --
 kernel/nativevalues.ml    | 27 ---------------------------
 kernel/safe_typing.ml     |  7 -------
 kernel/term.ml            | 11 -----------
 lib/heap.ml               |  2 --
 library/loadpath.ml       |  4 ----
 pretyping/evarsolve.ml    | 15 ---------------
 pretyping/pretyping.ml    | 14 --------------
 pretyping/tacred.ml       |  6 ------
 printing/ppconstr.ml      |  2 --
 printing/pptactic.ml      |  5 -----
 proofs/redexpr.ml         |  2 --
 stm/asyncTaskQueue.ml     |  4 +---
 tactics/auto.ml           |  3 ---
 tactics/class_tactics.ml  |  8 --------
 tactics/hints.ml          | 21 ---------------------
 tactics/tacinterp.ml      |  3 ---
 23 files changed, 1 insertion(+), 186 deletions(-)

diff --git a/engine/proofview_monad.ml b/engine/proofview_monad.ml
index a9faf0a83..88c5925ce 100644
--- a/engine/proofview_monad.ml
+++ b/engine/proofview_monad.ml
@@ -108,11 +108,6 @@ module Info = struct
   and compress f =
     CList.map_filter compress_tree f
 
-  let rec is_empty = let open Trace in function
-    | Seq(Dispatch,brs) -> List.for_all is_empty brs
-    | Seq(DBranch,br) -> List.for_all is_empty br
-    | _ -> false
-
   (** [with_sep] is [true] when [Tactic m] must be printed with a
       trailing semi-colon. *)
   let rec pr_tree with_sep = let open Trace in function
diff --git a/ide/coq.ml b/ide/coq.ml
index a60f327b4..268a95a33 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -99,9 +99,6 @@ let display_coqtop_answer cmd lines =
      "Command was: "^cmd^"\n"^
      "Answer was: "^(String.concat "\n  " lines))
 
-let check_remaining_opt arg =
-  if arg <> "" && arg.[0] = '-' then fatal_error_popup ("Illegal option: "^arg)
-
 let rec filter_coq_opts args =
   let argstr = String.concat " " (List.map Filename.quote args) in
   let cmd = Filename.quote (coqtop_path ()) ^" -nois -filteropts " ^ argstr in
@@ -200,8 +197,6 @@ module GlibMainLoop = struct
   let read_all = Ideutils.io_read_all
   let async_chan_of_file fd = Glib.Io.channel_of_descr fd
   let async_chan_of_socket s = !gio_channel_of_descr_socket s
-  let add_timeout ~sec callback =
-    ignore(Glib.Timeout.add ~ms:(sec * 1000) ~callback)
 end
 
 module CoqTop = Spawn.Async(GlibMainLoop)
diff --git a/ide/document.ml b/ide/document.ml
index 41d5a7564..bb431e791 100644
--- a/ide/document.ml
+++ b/ide/document.ml
@@ -124,12 +124,6 @@ let context d =
   let pair _ x y = try Option.get x, y with Option.IsNone -> assert false in
   List.map (flat pair true) top, List.map (flat pair true) bot
 
-let iter d f =
-  let a, s, b = to_lists d in
-  List.iter (flat f false) a;
-  List.iter (flat f true)  s;
-  List.iter (flat f false) b
-  
 let stateid_opt_equal = Option.equal Stateid.equal
 
 let is_in_focus d id =
diff --git a/ide/wg_ProofView.ml b/ide/wg_ProofView.ml
index 148add6e9..642a57787 100644
--- a/ide/wg_ProofView.ml
+++ b/ide/wg_ProofView.ml
@@ -114,19 +114,6 @@ let mode_tactic sel_cb (proof : #GText.view_skel) goals hints = match goals with
                          (Some Tags.Proof.goal)));
       ignore(proof#scroll_to_mark ~use_align:true ~yalign:0.95 `INSERT)
 
-let mode_cesar (proof : #GText.view_skel) = function
-  | [] -> assert false
-  | { Interface.goal_hyp = hyps; Interface.goal_ccl = cur_goal; } :: _ ->
-      proof#buffer#insert "    *** Declarative Mode ***\n";
-      List.iter
-        (fun hyp -> insert_xml proof#buffer hyp; proof#buffer#insert "\n")
-        hyps;
-      proof#buffer#insert "______________________________________\n";
-      proof#buffer#insert "thesis := \n ";
-      insert_xml proof#buffer cur_goal;
-      proof#buffer#insert "\n";
-      ignore (proof#scroll_to_iter (proof#buffer#get_iter_at_mark `INSERT))
-
 let rec flatten = function
 | [] -> []
 | (lg, rg) :: l ->
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index ed85c38de..5c9e80df3 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -462,15 +462,6 @@ let is_needed_for_correct_partial_application tail imp =
 
 exception Expl
 
-let params_implicit n impl = 
-  let rec aux n impl =
-    if n == 0 then true
-    else match impl with
-    | [] -> false
-    | imp :: impl when is_status_implicit imp -> aux (pred n) impl
-    | _ -> false
-  in aux n impl
-
 (* Implicit args indexes are in ascending order *)
 (* inctx is useful only if there is a last argument to be deduced from ctxt *)
 let explicitize loc inctx impl (cf,f) args =
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index d4cb79775..f9de8c466 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -698,19 +698,6 @@ let intern_var genv (ltacvars,ntnvars) namedctx loc id =
 	(* [id] a goal variable *)
 	GVar (loc,id), [], [], []
 
-let proj_impls r impls =
-  let env = Global.env () in
-  let f (x, l) = x, projection_implicits env r l in
-    List.map f impls
-
-let proj_scopes n scopes = 
-  List.skipn_at_least n scopes
-
-let proj_impls_scopes p impls scopes =
-  match p with
-  | Some (r, n) -> proj_impls r impls, proj_scopes n scopes
-  | None -> impls, scopes
-
 let find_appl_head_data c =
   match c with
   | GRef (loc,ref,_) as x -> 
diff --git a/kernel/declareops.ml b/kernel/declareops.ml
index 73cfd0122..803df7827 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 40bef4bc6..6e097b613 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 c7ab6491d..33aa2972b 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 455248dd5..2060c7b6e 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 =
diff --git a/lib/heap.ml b/lib/heap.ml
index a19bc0d1c..5682b87bb 100644
--- a/lib/heap.ml
+++ b/lib/heap.ml
@@ -62,8 +62,6 @@ module Functional(X : Ordered) = struct
 
   let empty = Leaf
 
-  let is_empty t = t = Leaf
-
   let rec add x = function
     | Leaf ->
         Node (Leaf, x, Leaf)
diff --git a/library/loadpath.ml b/library/loadpath.ml
index 16b419454..f77bd1ef5 100644
--- a/library/loadpath.ml
+++ b/library/loadpath.ml
@@ -84,10 +84,6 @@ let add_load_path phys_path coq_path ~implicit =
       end
   | _ -> anomaly_too_many_paths phys_path
 
-let extend_path_with_dirpath p dir =
-  List.fold_left Filename.concat p
-    (List.rev_map Id.to_string (DirPath.repr dir))
-
 let filter_path f =
   let rec aux = function
   | [] -> []
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index fe26dcd28..69e8e9d98 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -1007,21 +1007,6 @@ let postpone_non_unique_projection env evd pbty (evk,argsv as ev) sols rhs =
  * Note: argument f is the function used to instantiate evars.
  *)
 
-let are_canonical_instances args1 args2 env =
-  let n1 = Array.length args1 in
-  let n2 = Array.length args2 in
-  let rec aux n = function
-    | (id,_,c)::sign
-        when n < n1 && isVarId id args1.(n) && isVarId id args2.(n) ->
-        aux (n+1) sign
-    | [] ->
-        let rec aux2 n =
-          Int.equal n n1 ||
-          (isRelN (n1-n) args1.(n) && isRelN (n1-n) args2.(n) && aux2 (n+1))
-        in aux2 n
-    | _ -> false in
-  Int.equal n1 n2 && aux 0 (named_context env)
-
 let filter_compatible_candidates conv_algo env evd evi args rhs c =
   let c' = instantiate_evar_array evi c args in
   match conv_algo env evd Reduction.CONV rhs c' with
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index f5b89e789..7d5496917 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -444,26 +444,12 @@ let new_type_evar env evdref loc =
       univ_flexible_alg ~src:(loc,Evar_kinds.InternalHole)) evdref
   in e
 
-let get_projection env cst =
-  let cb = lookup_constant cst env in
-    match cb.Declarations.const_proj with
-    | Some {Declarations.proj_ind = mind; proj_npars = n;
-	    proj_arg = m; proj_type = ty} -> 
-      (cst,mind,n,m,ty)
-    | None -> raise Not_found
-
 let (f_genarg_interp, genarg_interp_hook) = Hook.make ()
 
 (* [pretype tycon env evdref lvar lmeta cstr] attempts to type [cstr] *)
 (* in environment [env], with existential variables [evdref] and *)
 (* the type constraint tycon *)
 
-let is_GHole = function
-  | GHole _ -> true
-  | _ -> false
-
-let evars = ref Id.Map.empty
-
 let rec pretype k0 resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_var_map) t =
   let inh_conv_coerce_to_tycon = inh_conv_coerce_to_tycon resolve_tc in
   let pretype_type = pretype_type k0 resolve_tc in
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index 48911a5a9..31e75e550 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -940,8 +940,6 @@ let matches_head env sigma c t =
     | Proj (p, _) -> Constr_matching.matches env sigma c (mkConst (Projection.constant p))
     | _ -> raise Constr_matching.PatternMatchingFailure
 
-let is_pattern_meta = function Pattern.PMeta _ -> true | _ -> false
-
 (** FIXME: Specific function to handle projections: it ignores what happens on the
     parameters. This is a temporary fix while rewrite etc... are not up to equivalence
     of the projection and its eta expanded form.
@@ -1055,10 +1053,6 @@ let unfold env sigma name =
   else
     error (string_of_evaluable_ref env name^" is opaque.")
 
-let is_projection env = function
-  | EvalVarRef _ -> false
-  | EvalConstRef c -> Environ.is_projection c env
-
 (* [unfoldoccs : (readable_constraints -> (int list * full_path) -> constr -> constr)]
  * Unfolds the constant name in a term c following a list of occurrences occl.
  * at the occurrences of occ_list. If occ_list is empty, unfold all occurrences.
diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml
index d15c3ee2f..c07057a09 100644
--- a/printing/ppconstr.ml
+++ b/printing/ppconstr.ml
@@ -136,8 +136,6 @@ end) = struct
 
   let pr_sep_com sep f c = pr_with_comments (constr_loc c) (sep() ++ f c)
 
-  let pr_in_comment pr x = str "(* " ++ pr x ++ str " *)"
-
   let pr_univ l =
     match l with
       | [_,x] -> str x
diff --git a/printing/pptactic.ml b/printing/pptactic.ml
index 7800f1edb..a5716279f 100644
--- a/printing/pptactic.ml
+++ b/printing/pptactic.ml
@@ -685,11 +685,6 @@ module Make
     | l -> spc () ++
       hov 2 (keyword "using" ++ spc () ++ prlist_with_sep pr_comma prc l)
 
-  let string_of_debug = function
-    | Off -> ""
-    | Debug -> "debug "
-    | Info -> "info_"
-
   let pr_then () = str ";"
 
   let ltop = (5,E)
diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml
index be92f2b04..89ecdb0df 100644
--- a/proofs/redexpr.ml
+++ b/proofs/redexpr.ml
@@ -158,8 +158,6 @@ let make_flag env f =
 	  f.rConst red
   in red
 
-let is_reference = function PRef _ | PVar _ -> true | _ -> false
-
 (* table of custom reductino fonctions, not synchronized,
    filled via ML calls to [declare_reduction] *)
 let reduction_tab = ref String.Map.empty
diff --git a/stm/asyncTaskQueue.ml b/stm/asyncTaskQueue.ml
index e525031e6..863bab7cc 100644
--- a/stm/asyncTaskQueue.ml
+++ b/stm/asyncTaskQueue.ml
@@ -60,9 +60,7 @@ module Make(T : Task) = struct
 
   type more_data =
     | MoreDataUnivLevel of Univ.universe_level list
- 
-  let request_expiry_of_task (t, c) = T.request_of_task t, c
-  
+
   let slave_respond (Request r) =
     let res = T.perform r in
     Response res
diff --git a/tactics/auto.ml b/tactics/auto.ml
index e6263f92c..d6552920f 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -67,9 +67,6 @@ let auto_unif_flags_of st1 st2 useeager =
 let auto_unif_flags =
   auto_unif_flags_of full_transparent_state empty_transparent_state false
 
-let auto_flags_of_state st =
-  auto_unif_flags_of full_transparent_state st false
-
 (* Try unification with the precompiled clause, then use registered Apply *)
 
 let connect_hint_clenv poly (c, _, ctx) clenv gl =
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index 4f0ffa024..8cd7b1ad6 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -569,14 +569,6 @@ let rec fix_limit limit (t : 'a tac) : 'a tac =
   if Int.equal limit 0 then fail_tac ReachedLimit
   else then_tac t { skft = fun sk fk -> (fix_limit (pred limit) t).skft sk fk }
 
-let fix_iterative' t =
-  let rec aux depth =
-    { skft = fun sk fk gls -> 
-      (fix_limit depth t).skft sk
-	(function NotApplicable as e -> fk e
-	  | ReachedLimit -> (aux (succ depth)).skft sk fk gls) gls }
-  in aux 1
-
 let fix_iterative t =
   let rec aux depth =
     or_else_tac (fix_limit depth t)
diff --git a/tactics/hints.ml b/tactics/hints.ml
index 6d623f1c3..8d8b5fcc6 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -154,27 +154,6 @@ let fresh_key =
     in
     KerName.make mp dir (Label.of_id lbl)
 
-let eq_hints_path_atom p1 p2 = match p1, p2 with
-| PathHints gr1, PathHints gr2 -> List.equal eq_gr gr1 gr2
-| PathAny, PathAny -> true
-| (PathHints _ | PathAny), _ -> false
-
-let eq_auto_tactic t1 t2 = match t1, t2 with
-| Res_pf (c1, _), Res_pf (c2, _) -> Constr.equal c1 c2
-| ERes_pf (c1, _), ERes_pf (c2, _) -> Constr.equal c1 c2
-| Give_exact (c1, _), Give_exact (c2, _) -> Constr.equal c1 c2
-| Res_pf_THEN_trivial_fail (c1, _), Res_pf_THEN_trivial_fail (c2, _) -> Constr.equal c1 c2
-| Unfold_nth gr1, Unfold_nth gr2 -> eq_egr gr1 gr2
-| Extern tac1, Extern tac2 -> tac1 == tac2 (** May cause redundancy in addkv *)
-| (Res_pf _ | ERes_pf _ | Give_exact _ | Res_pf_THEN_trivial_fail _
-  | Unfold_nth _ | Extern _), _ -> false
-
-let eq_hint_metadata t1 t2 =
-  Int.equal t1.pri t2.pri &&
-  Option.equal constr_pattern_eq t1.pat t2.pat &&
-  eq_hints_path_atom t1.name t2.name &&
-  eq_auto_tactic t1.code t2.code
-
 let pri_order_int (id1, {pri=pri1}) (id2, {pri=pri2}) =
   let d = pri1 - pri2 in
     if Int.equal d 0 then id2 - id1
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index a87181588..5450a00f4 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -1115,9 +1115,6 @@ let rec read_match_rule lfun ist env sigma = function
 
 (* misc *)
 
-let mk_hyp_value ist env sigma c =
-  (mkVar (interp_hyp ist env sigma c))
-
 let interp_focussed wit f v =
   Ftactic.nf_enter begin fun gl ->
     let v = Genarg.out_gen (glbwit wit) v in
-- 
cgit v1.2.3