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

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

(limited to 'plugins')

diff --git a/plugins/ltac/g_ltac.mlg b/plugins/ltac/g_ltac.mlg
index b1b96ea9a7..3da5b2bfc4 100644
--- a/plugins/ltac/g_ltac.mlg
+++ b/plugins/ltac/g_ltac.mlg
@@ -147,7 +147,7 @@ GRAMMAR EXTEND Gram
       | IDENT "solve" ; "["; l = LIST0 ltac_expr SEP "|"; "]" ->
           { TacSolve l }
       | IDENT "idtac"; l = LIST0 message_token -> { TacId l }
-      | g=failkw; n = [ n = int_or_var -> { n } | -> { fail_default_value } ];
+      | g=failkw; n = [ n = nat_or_var -> { n } | -> { fail_default_value } ];
           l = LIST0 message_token -> { TacFail (g,n,l) }
       | st = simple_tactic -> { st }
       | a = tactic_value -> { TacArg(CAst.make ~loc a) }
-- 
cgit v1.2.3