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, 35 deletions

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