From 92ddd42345f9976a1e3b2cc2e53541ef0864ed0b Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 27 Sep 2020 07:35:28 +0200
Subject: Deprecating wit_var to the benefit of its synonymous wit_hyp.

Note: "hyp" was documented in Ltac Notation chapter but "var" was not.
---
 plugins/ltac/pptactic.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins/ltac/pptactic.ml')

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
-- 
cgit v1.2.3