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/common.edit_mlg | 4 ++--
 doc/tools/docgram/fullGrammar     | 2 +-
 doc/tools/docgram/orderedGrammar  | 2 +-
 3 files changed, 4 insertions(+), 4 deletions(-)

(limited to 'doc/tools/docgram')

diff --git a/doc/tools/docgram/common.edit_mlg b/doc/tools/docgram/common.edit_mlg
index f267cdb697..44bb767011 100644
--- a/doc/tools/docgram/common.edit_mlg
+++ b/doc/tools/docgram/common.edit_mlg
@@ -864,8 +864,8 @@ ltac_expr1: [
 | EDIT match_key ADD_OPT "reverse" "goal" "with" match_context_list "end"
 | MOVETO simple_tactic match_key OPT "reverse" "goal" "with" match_context_list "end"
 | MOVETO simple_tactic match_key ltac_expr5 "with" match_list "end"
-| REPLACE failkw [ int_or_var | ] LIST0 message_token
-| WITH failkw OPT int_or_var LIST0 message_token
+| REPLACE failkw [ nat_or_var | ] LIST0 message_token
+| WITH failkw OPT nat_or_var LIST0 message_token
 | REPLACE reference LIST0 tactic_arg
 | WITH reference LIST1 tactic_arg
 | l1_tactic
diff --git a/doc/tools/docgram/fullGrammar b/doc/tools/docgram/fullGrammar
index ccf38d2c15..9f2559ffbc 100644
--- a/doc/tools/docgram/fullGrammar
+++ b/doc/tools/docgram/fullGrammar
@@ -2095,7 +2095,7 @@ ltac_expr1: [
 | "first" "[" LIST0 ltac_expr5 SEP "|" "]"
 | "solve" "[" LIST0 ltac_expr5 SEP "|" "]"
 | "idtac" LIST0 message_token
-| failkw [ int_or_var | ] LIST0 message_token
+| failkw [ nat_or_var | ] LIST0 message_token
 | simple_tactic
 | tactic_value
 | reference LIST0 tactic_arg
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