diff options
| author | Pierre-Marie Pédrot | 2020-10-15 15:15:44 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-10-15 15:15:44 +0200 |
| commit | 476520ab32d3e975f6cee8aabcd04ad5fdfbbd77 (patch) | |
| tree | e8a75d0411c275635540f675449cc38b00c989fd /plugins/ltac/pptactic.ml | |
| parent | 4bf43453ec5f635ae87a2edeb4f51d95f2d5ac67 (diff) | |
| parent | 92ddd42345f9976a1e3b2cc2e53541ef0864ed0b (diff) | |
Merge PR #13098: Deprecating wit_var to the benefit of its synonymous wit_hyp
Reviewed-by: ejgallego
Reviewed-by: gares
Ack-by: jfehrle
Reviewed-by: ppedrot
Diffstat (limited to 'plugins/ltac/pptactic.ml')
| -rw-r--r-- | plugins/ltac/pptactic.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml index cbb53497d3..fe896f9351 100644 --- a/plugins/ltac/pptactic.ml +++ b/plugins/ltac/pptactic.ml @@ -1323,7 +1323,7 @@ let () = 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_basic_print0 wit_hyp pr_lident pr_lident pr_id; 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 |