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/pptactic.ml | 13 ++++++++----- 1 file changed, 8 insertions(+), 5 deletions(-) (limited to 'plugins/ltac/pptactic.ml') diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml index 79f0f521cc..bf0ce1e964 100644 --- a/plugins/ltac/pptactic.ml +++ b/plugins/ltac/pptactic.ml @@ -1314,6 +1314,12 @@ let pr_glob_constr_pptac env sigma c = let pr_lglob_constr_pptac env sigma c = pr_lglob_constr_env env c +let pr_raw_intro_pattern = + lift_env (fun env sigma -> Miscprint.pr_intro_pattern @@ pr_constr_expr env sigma) + +let pr_glob_intro_pattern = + lift_env (fun env sigma -> Miscprint.pr_intro_pattern (fun (c,_) -> pr_glob_constr_pptac env sigma c)) + let () = let pr_bool b = if b then str "true" else str "false" in let pr_unit _ = str "()" in @@ -1323,11 +1329,8 @@ let () = pr_qualid (pr_or_var (pr_located pr_global)) pr_global; register_basic_print0 wit_ident pr_id pr_id pr_id; register_basic_print0 wit_var pr_lident pr_lident pr_id; - register_print0 - wit_intro_pattern - (lift_env (fun env sigma -> Miscprint.pr_intro_pattern @@ pr_constr_expr env sigma)) - (lift_env (fun env sigma -> Miscprint.pr_intro_pattern (fun (c,_) -> pr_glob_constr_pptac env sigma c))) - pr_intro_pattern_env; + register_print0 wit_intropattern pr_raw_intro_pattern pr_glob_intro_pattern pr_intro_pattern_env [@warning "-3"]; + register_print0 wit_simple_intropattern pr_raw_intro_pattern pr_glob_intro_pattern pr_intro_pattern_env; Genprint.register_print0 wit_clause_dft_concl (lift (pr_clauses (Some true) pr_lident)) -- cgit v1.2.3