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/extraargs.mlg | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'plugins/ltac/extraargs.mlg')

diff --git a/plugins/ltac/extraargs.mlg b/plugins/ltac/extraargs.mlg
index 863c4d37d8..ad4374dba3 100644
--- a/plugins/ltac/extraargs.mlg
+++ b/plugins/ltac/extraargs.mlg
@@ -47,7 +47,7 @@ let () =
 
 let () =
   let register name entry = Tacentries.register_tactic_notation_entry name entry in
-  register "hyp" wit_var;
+  register "hyp" wit_hyp;
   register "simple_intropattern" wit_simple_intropattern;
   register "integer" wit_integer;
   register "reference" wit_ref;
@@ -140,7 +140,7 @@ ARGUMENT EXTEND occurrences
   GLOB_PRINTED BY { pr_occurrences }
 
 | [ ne_integer_list(l) ] -> { ArgArg l }
-| [ var(id) ] -> { ArgVar id }
+| [ hyp(id) ] -> { ArgVar id }
 END
 
 {
-- 
cgit v1.2.3