From 70b18cd58243c99b13eefbd9c593b0f3929c742c Mon Sep 17 00:00:00 2001
From: Jim Fehrle
Date: Tue, 24 Nov 2020 15:09:28 -0800
Subject: Use nat_or_var for fail/gfail

---
 doc/tools/docgram/orderedGrammar | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'doc/tools/docgram/orderedGrammar')

diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar
index 72e101446c..b53af609ec 100644
--- a/doc/tools/docgram/orderedGrammar
+++ b/doc/tools/docgram/orderedGrammar
@@ -1653,7 +1653,7 @@ simple_tactic: [
 | "first" "[" LIST0 ltac_expr SEP "|" "]"
 | "solve" "[" LIST0 ltac_expr SEP "|" "]"
 | "idtac" LIST0 [ ident | string | natural ]
-| [ "fail" | "gfail" ] OPT int_or_var LIST0 [ ident | string | natural ]
+| [ "fail" | "gfail" ] OPT nat_or_var LIST0 [ ident | string | natural ]
 | ltac_expr ssrintros      (* SSR plugin *)
 | "fun" LIST1 name "=>" ltac_expr
 | "eval" red_expr "in" term
-- 
cgit v1.2.3