From 92bc869c2cec1ffb7e2d0bfcc6b64147718fbe87 Mon Sep 17 00:00:00 2001
From: Pierre Roux
Date: Tue, 8 Sep 2020 10:41:03 +0200
Subject: Turn integer into natural in several mlgs

Negative values had no meaning there.
Those were spotted by Hugo Herbelin while reviewing #12979 .
---
 user-contrib/Ltac2/g_ltac2.mlg | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'user-contrib')

diff --git a/user-contrib/Ltac2/g_ltac2.mlg b/user-contrib/Ltac2/g_ltac2.mlg
index bec9632e84..d42a935104 100644
--- a/user-contrib/Ltac2/g_ltac2.mlg
+++ b/user-contrib/Ltac2/g_ltac2.mlg
@@ -371,7 +371,7 @@ GRAMMAR EXTEND Gram
   ;
   syn_level:
     [ [ -> { None }
-      | ":"; n = Prim.integer -> { Some n }
+      | ":"; n = Prim.natural -> { Some n }
     ] ]
   ;
   tac2def_syn:
-- 
cgit v1.2.3