diff options
| author | Théo Zimmermann | 2019-06-19 10:41:09 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2019-06-19 10:41:09 +0200 |
| commit | cdba5f7ceee1adfbdd96ffc82115fbc1e6750b80 (patch) | |
| tree | e4e94c235b18bdf96b82db071da74535ccd827c5 /plugins/ltac/pptactic.ml | |
| parent | 415e83efb9e767ddf65b8c27d4e497592fd61f2c (diff) | |
| parent | 459b5ce5b2b825db43d645357f83d7fe17289bc5 (diff) | |
Merge PR #10239: Deprecate grammar entry "intropattern" in tactic notations in favor of "simple_intropattern"
Reviewed-by: Zimmi48
Reviewed-by: ppedrot
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 4b6b192f0a..db8d09b79e 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)) |