From a181ea2fce1177cc33cd7fdf504d69fff15c7e97 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 24 May 2020 18:13:12 +0200
Subject: Remove the prolog tactic.

It was deprecated in 8.12 and not used in the wild.
---
 plugins/ltac/g_auto.mlg | 5 -----
 1 file changed, 5 deletions(-)

(limited to 'plugins')

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)
-- 
cgit v1.2.3