diff options
| author | Pierre-Marie Pédrot | 2020-05-24 18:13:12 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-05-25 08:05:39 +0200 |
| commit | a181ea2fce1177cc33cd7fdf504d69fff15c7e97 (patch) | |
| tree | e0c9183c9f88fe5b3fadbf9935ee237e74423451 | |
| parent | 16e0877c6e3ec6228875e10afb1ec17d640eb1e9 (diff) | |
Remove the prolog tactic.
It was deprecated in 8.12 and not used in the wild.
| -rw-r--r-- | plugins/ltac/g_auto.mlg | 5 | ||||
| -rw-r--r-- | tactics/eauto.ml | 25 | ||||
| -rw-r--r-- | tactics/eauto.mli | 2 |
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 |