diff options
| author | Pierre-Marie Pédrot | 2020-05-11 12:18:40 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-05-11 12:18:40 +0200 |
| commit | 0abac9befe6f165dd7829430a229192e6cb18453 (patch) | |
| tree | 744c8d39701f3226c4fc3bdbaafc10bada0b2de7 /plugins/ltac/pptactic.ml | |
| parent | aab47903fb2d3e0085b03d5ade94f4ae644cd76c (diff) | |
| parent | 6e4ebb2dbaa2cb9eb70ce205386bee08c80aaa00 (diff) | |
Merge PR #12129: Add a `with_strategy` tactic
Ack-by: Zimmi48
Ack-by: ejgallego
Ack-by: herbelin
Ack-by: ppedrot
Diffstat (limited to 'plugins/ltac/pptactic.ml')
| -rw-r--r-- | plugins/ltac/pptactic.ml | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml index 09f1fc371a..d74e981c6d 100644 --- a/plugins/ltac/pptactic.ml +++ b/plugins/ltac/pptactic.ml @@ -1325,6 +1325,8 @@ let () = register_basic_print0 wit_int_or_var (pr_or_var int) (pr_or_var int) int; register_basic_print0 wit_ref pr_qualid (pr_or_var (pr_located pr_global)) pr_global; + register_basic_print0 wit_smart_global + (pr_or_by_notation 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_intropattern pr_raw_intro_pattern pr_glob_intro_pattern pr_intro_pattern_env [@warning "-3"]; |