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 ++++--
 interp/stdarg.mli | 3 +++
 2 files changed, 7 insertions(+), 2 deletions(-)

(limited to 'interp')

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"
 
diff --git a/interp/stdarg.mli b/interp/stdarg.mli
index 3ae8b7d73f..bd34af5543 100644
--- a/interp/stdarg.mli
+++ b/interp/stdarg.mli
@@ -37,7 +37,10 @@ val wit_int_or_var : (int or_var, int or_var, int) genarg_type
 
 val wit_ident : Id.t uniform_genarg_type
 
+val wit_hyp : (lident, lident, Id.t) genarg_type
+
 val wit_var : (lident, lident, Id.t) genarg_type
+[@@ocaml.deprecated "Use Stdarg.wit_hyp"]
 
 val wit_ref : (qualid, GlobRef.t located or_var, GlobRef.t) genarg_type
 
-- 
cgit v1.2.3