From 41b07808c84a86ea4b77e0c7855b22bfd3906669 Mon Sep 17 00:00:00 2001
From: Jim Fehrle
Date: Mon, 12 Oct 2020 21:55:00 -0700
Subject: Rename misc nonterminals

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

(limited to 'plugins/funind')

diff --git a/plugins/funind/g_indfun.mlg b/plugins/funind/g_indfun.mlg
index bbc4df7dde..4b46e09e57 100644
--- a/plugins/funind/g_indfun.mlg
+++ b/plugins/funind/g_indfun.mlg
@@ -159,7 +159,7 @@ GRAMMAR EXTEND Gram
   GLOBAL: function_rec_definition_loc ;
 
   function_rec_definition_loc:
-    [ [ g = Vernac.rec_definition -> { Loc.tag ~loc g } ]]
+    [ [ g = Vernac.fix_definition -> { Loc.tag ~loc g } ]]
     ;
 
 END
-- 
cgit v1.2.3