From 232f67d20218a593bbd196d8a5e063b80487c599 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 28 Feb 2020 10:49:47 +0100
Subject: Deprecate the "prolog" tactic.

It was not documented, I do not think it is used in the wild, and it relies
on legacy code. As solid conjunction of reasons that support its deprecation.
---
 plugins/ltac/g_auto.mlg | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

(limited to 'plugins')

diff --git a/plugins/ltac/g_auto.mlg b/plugins/ltac/g_auto.mlg
index 8344f9dae3..82c64a9857 100644
--- a/plugins/ltac/g_auto.mlg
+++ b/plugins/ltac/g_auto.mlg
@@ -114,7 +114,7 @@ END
 
 (** Eauto *)
 
-TACTIC EXTEND prolog
+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
@@ -253,4 +253,3 @@ VERNAC COMMAND EXTEND HintCut CLASSIFIED AS SIDEFF
           (match dbnames with None -> ["core"] | Some l -> l) entry;
  }
 END
-
-- 
cgit v1.2.3