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.
---
 interp/stdarg.ml | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

(limited to 'interp/stdarg.ml')

diff --git a/interp/stdarg.ml b/interp/stdarg.ml
index 343f85be03..70be55f843 100644
--- a/interp/stdarg.ml
+++ b/interp/stdarg.ml
@@ -40,8 +40,10 @@ let wit_int_or_var =
 let wit_ident =
   make0 "ident"
 
-let wit_var =
-  make0 ~dyn:(val_tag (topwit wit_ident)) "var"
+let wit_hyp =
+  make0 ~dyn:(val_tag (topwit wit_ident)) "hyp"
+
+let wit_var = wit_hyp
 
 let wit_ref = make0 "ref"
 
-- 
cgit v1.2.3