3 files changed, 0 insertions, 32 deletions
diff --git a/plugins/ltac/g_auto.mlg b/plugins/ltac/g_auto.mlg
index b4527694ae..2e72ceae5a 100644
--- a/plugins/ltac/g_auto.mlg
+++ b/plugins/ltac/g_auto.mlg
@@ -114,11 +114,6 @@ END
 
 (** Eauto *)
 
-TACTIC EXTEND prolog DEPRECATED { Deprecation.make ~note:"Use eauto instead" () }
-| [ "prolog" "[" uconstr_list(l) "]" int_or_var(n) ] ->
-    { Eauto.prolog_tac (eval_uconstrs ist l) n }
-END
-
 {
 
 let make_depth n = snd (Eauto.make_dimension n None)
diff --git a/tactics/eauto.ml b/tactics/eauto.ml
index 710e0a6808..7d8620468d 100644
--- a/tactics/eauto.ml
+++ b/tactics/eauto.ml
@@ -77,31 +77,6 @@ let apply_tac_list tac glls =
       re_sig (pack.it @ rest) pack.sigma
   | _ -> user_err Pp.(str "apply_tac_list")
 
-let one_step l gl =
-  [Proofview.V82.of_tactic Tactics.intro]
-  @ (List.map (fun c -> Proofview.V82.of_tactic (Tactics.Simple.eapply c)) (List.map mkVar (pf_ids_of_hyps gl)))
-  @ (List.map (fun c -> Proofview.V82.of_tactic (Tactics.Simple.eapply c)) l)
-  @ (List.map (fun c -> Proofview.V82.of_tactic (assumption c)) (pf_ids_of_hyps gl))
-
-let rec prolog l n gl =
-  if n <= 0 then user_err Pp.(str "prolog - failure");
-  let prol = (prolog l (n-1)) in
-  (tclFIRST (List.map (fun t -> (tclTHEN t prol)) (one_step l gl))) gl
-
-let prolog_tac l n =
-  Proofview.V82.tactic begin fun gl ->
-  let map c =
-    let (sigma, c) = c (pf_env gl) (project gl) in
-    (* Dropping the universe context is probably wrong *)
-    let (c, _) = pf_apply (prepare_hint false) gl (sigma, c) in
-    c
-  in
-  let l = List.map map l in
-  try (prolog l n gl)
-  with UserError (Some "Refiner.tclFIRST",_) ->
-    user_err ~hdr:"Prolog.prolog" (str "Prolog failed.")
-  end
-
 open Auto
 
 (***************************************************************************)
diff --git a/tactics/eauto.mli b/tactics/eauto.mli
index e6f2c1a8e2..5fb038a767 100644
--- a/tactics/eauto.mli
+++ b/tactics/eauto.mli
@@ -18,8 +18,6 @@ val registered_e_assumption : unit Proofview.tactic
 
 val e_give_exact : ?flags:Unification.unify_flags -> constr -> unit Proofview.tactic
 
-val prolog_tac : delayed_open_constr list -> int -> unit Proofview.tactic
-
 val gen_eauto : ?debug:debug -> bool * int -> delayed_open_constr list ->
   hint_db_name list option -> unit Proofview.tactic