From 459b5ce5b2b825db43d645357f83d7fe17289bc5 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Fri, 24 May 2019 20:53:14 +0200
Subject: Deprecate "intro_pattern" in tactic notations in favor of
 "simple_intropattern".

This is to prevent confusion with the terminology used in the grammar
of tactic in the reference manual: "intropattern" in Tactic Notation
and TACTIC EXTEND is actually bound to simple_intropattern and not to
what is called intropattern in the reference manual

After some deprecation phase, "intropattern" could be added back to
mean the "intropattern" of the reference manual.

Note that "simple_intropattern" is actually already available in
"Tactic Notation" with the correct meaning as an entry. Only
"intropattern" is misguiding.
---
 plugins/ltac/tacinterp.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'plugins/ltac/tacinterp.ml')

diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index 4a0b01bcdc..d5cb0cad50 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -2029,7 +2029,8 @@ let () =
   register_interp0 wit_pre_ident (lift interp_pre_ident);
   register_interp0 wit_ident (lift interp_ident);
   register_interp0 wit_var (lift interp_hyp);
-  register_interp0 wit_intro_pattern (lifts interp_intro_pattern);
+  register_interp0 wit_intropattern (lifts interp_intro_pattern) [@warning "-3"];
+  register_interp0 wit_simple_intropattern (lifts interp_intro_pattern);
   register_interp0 wit_clause_dft_concl (lift interp_clause);
   register_interp0 wit_constr (lifts interp_constr);
   register_interp0 wit_tacvalue (fun ist v -> Ftactic.return v);
-- 
cgit v1.2.3