diff options
| author | Hugo Herbelin | 2019-05-24 20:53:14 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2019-06-16 20:58:50 +0200 |
| commit | 459b5ce5b2b825db43d645357f83d7fe17289bc5 (patch) | |
| tree | 45dd0a7a3d07bda0292c5f4bedd1b9e0bae858a1 /plugins/ltac/pptactic.ml | |
| parent | 6eba5b5ba91f9ec02b809e0c223324e0f4fdbf85 (diff) | |
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.
Diffstat (limited to 'plugins/ltac/pptactic.ml')
| -rw-r--r-- | plugins/ltac/pptactic.ml | 13 |
1 files changed, 8 insertions, 5 deletions
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)) |