From 7ebcbc1cecca87619aa4b01606021c29c5d1f0a2 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Fri, 28 Feb 2020 20:19:00 +0100
Subject: [parser] lk_int -> lk_nat

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

(limited to 'plugins')

diff --git a/plugins/ltac/g_tactic.mlg b/plugins/ltac/g_tactic.mlg
index 517c0d59e1..3e4c7ba782 100644
--- a/plugins/ltac/g_tactic.mlg
+++ b/plugins/ltac/g_tactic.mlg
@@ -54,7 +54,7 @@ let test_lpar_id_rpar =
 let test_lpar_idnum_coloneq =
   let open Pcoq.Lookahead in
   to_entry "test_lpar_idnum_coloneq" begin
-    lk_kw "(" >> (lk_ident <+> lk_int) >> lk_kw ":="
+    lk_kw "(" >> (lk_ident <+> lk_nat) >> lk_kw ":="
   end
 
 (* idem for (x:t) *)
-- 
cgit v1.2.3