Use nat_or_var for fail/gfail

5 files changed, 11 insertions, 6 deletions

diff --git a/doc/changelog/04-tactics/13469-no-int-in-fail.rst b/doc/changelog/04-tactics/13469-no-int-in-fail.rst
new file mode 100644
index 0000000000..e0fcbb924e
--- /dev/null
+++ b/doc/changelog/04-tactics/13469-no-int-in-fail.rst
@@ -0,0 +1,5 @@
+- **Removed:**
+  :tacn:`fail` and :tacn:`gfail`, which formerly accepted negative
+  values as a parameter, now give syntax errors for negative
+  values (`#13469 <https://github.com/coq/coq/pull/13469>`_,
+  by Jim Fehrle).
diff --git a/doc/sphinx/proof-engine/ltac.rst b/doc/sphinx/proof-engine/ltac.rst
index 8b627c29a4..013ff0a83f 100644
--- a/doc/sphinx/proof-engine/ltac.rst
+++ b/doc/sphinx/proof-engine/ltac.rst
@@ -879,7 +879,7 @@ Print/identity tactic: idtac
 Failing
 ~~~~~~~
 
-.. tacn:: {| fail | gfail } {? @int_or_var } {* {| @ident | @string | @natural } }
+.. tacn:: {| fail | gfail } {? @nat_or_var } {* {| @ident | @string | @natural } }
    :name: fail; gfail
 
    :tacn:`fail` is the always-failing tactic: it does not solve any
@@ -900,7 +900,7 @@ Failing
    tactic into the goals, meaning that if there are no goals when it is
    evaluated, a tactic call like :tacn:`let` :n:`x := H in` :tacn:`fail` `0 x` will succeed.
 
-   :n:`@int_or_var`
+   :n:`@nat_or_var`
       The failure level. If no level is specified, it defaults to 0.
       The level is used by :tacn:`try`, :tacn:`repeat`, :tacn:`match goal` and the branching
       tacticals. If 0, it makes :tacn:`match goal` consider the next clause
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