aboutsummaryrefslogtreecommitdiff
path: root/toplevel
diff options
context:
space:
mode:
authorMaxime Dénès2020-02-28 20:19:00 +0100
committerMaxime Dénès2020-03-01 20:33:28 +0100
commit7ebcbc1cecca87619aa4b01606021c29c5d1f0a2 (patch)
tree082951992155940f3f6919568f5541e954aabfb8 /toplevel
parent38e57715c086183250dd6176f9eaad01bfcde4c5 (diff)
[parser] lk_int -> lk_nat
Diffstat (limited to 'toplevel')
-rw-r--r--toplevel/g_toplevel.mlg2
1 files changed, 1 insertions, 1 deletions
diff --git a/toplevel/g_toplevel.mlg b/toplevel/g_toplevel.mlg
index 09fc954fac..d3768eb1e3 100644
--- a/toplevel/g_toplevel.mlg
+++ b/toplevel/g_toplevel.mlg
@@ -36,7 +36,7 @@ let err () = raise Stream.Failure
let test_show_goal =
let open Pcoq.Lookahead in
to_entry "test_show_goal" begin
- lk_kw "Show" >> lk_kw "Goal" >> lk_int
+ lk_kw "Show" >> lk_kw "Goal" >> lk_nat
end
}