From a6d52d2502c09e8acdca464faf67d3956448cbcf Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 27 Sep 2020 10:46:48 +0200
Subject: Prim.pattern_ident takes a location and its synonymous
 pattern_identref is deprecated.

---
 plugins/ltac/g_tactic.mlg | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins')

diff --git a/plugins/ltac/g_tactic.mlg b/plugins/ltac/g_tactic.mlg
index e51b1f051d..c186a83a5c 100644
--- a/plugins/ltac/g_tactic.mlg
+++ b/plugins/ltac/g_tactic.mlg
@@ -280,7 +280,7 @@ GRAMMAR EXTEND Gram
       | "[="; tc = intropatterns; "]" -> { IntroInjection tc } ] ]
   ;
   naming_intropattern:
-    [ [ prefix = pattern_ident -> { IntroFresh prefix }
+    [ [ prefix = pattern_ident -> { IntroFresh prefix.CAst.v }
       | "?" -> { IntroAnonymous }
       | id = ident -> { IntroIdentifier id } ] ]
   ;
-- 
cgit v1.2.3