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/ssr/ssrcommon.ml  | 2 +-
 plugins/ssr/ssrparser.mlg | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

(limited to 'plugins/ssr')

diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml
index d859fe51ab..cb58b9bcb8 100644
--- a/plugins/ssr/ssrcommon.ml
+++ b/plugins/ssr/ssrcommon.ml
@@ -280,7 +280,7 @@ let interp_wit wit ist gl x =
   sigma, Tacinterp.Value.cast (topwit wit) arg
 
 let interp_hyp ist gl (SsrHyp (loc, id)) =
-  let s, id' = interp_wit wit_var ist gl CAst.(make ?loc id) in
+  let s, id' = interp_wit wit_hyp ist gl CAst.(make ?loc id) in
   if not_section_id id' then s, SsrHyp (loc, id') else
   hyp_err ?loc "Can't clear section hypothesis " id'
 
diff --git a/plugins/ssr/ssrparser.mlg b/plugins/ssr/ssrparser.mlg
index 89e0c9fcbe..7b584b5159 100644
--- a/plugins/ssr/ssrparser.mlg
+++ b/plugins/ssr/ssrparser.mlg
@@ -155,7 +155,7 @@ let pr_ssrhyp _ _ _ = pr_hyp
 let wit_ssrhyprep = add_genarg "ssrhyprep" (fun env sigma -> pr_hyp)
 
 let intern_hyp ist (SsrHyp (loc, id) as hyp) =
-  let _ = Tacintern.intern_genarg ist (in_gen (rawwit wit_var) CAst.(make ?loc id)) in
+  let _ = Tacintern.intern_genarg ist (in_gen (rawwit wit_hyp) CAst.(make ?loc id)) in
   if not_section_id id then hyp else
   hyp_err ?loc "Can't clear section hypothesis " id
 
-- 
cgit v1.2.3