diff options
Diffstat (limited to 'user-contrib')
| -rw-r--r-- | user-contrib/Ltac2/g_ltac2.mlg | 2 |
1 files changed, 1 insertions, 1 deletions
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: |