diff options
Diffstat (limited to 'plugins/ltac')
| -rw-r--r-- | plugins/ltac/g_tactic.mlg | 2 |
1 files changed, 1 insertions, 1 deletions
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) *) |