aboutsummaryrefslogtreecommitdiff
path: root/parsing/pcoq.mli
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 /parsing/pcoq.mli
parent38e57715c086183250dd6176f9eaad01bfcde4c5 (diff)
[parser] lk_int -> lk_nat
Diffstat (limited to 'parsing/pcoq.mli')
-rw-r--r--parsing/pcoq.mli2
1 files changed, 1 insertions, 1 deletions
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index 746510b911..6543a69b50 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -43,7 +43,7 @@ module Lookahead : sig
val check_no_space : t
val lk_kw : string -> t
val lk_kws : string list -> t
- val lk_int : t
+ val lk_nat : t
val lk_ident : t
val lk_ident_except : string list -> t
val lk_ident_list : t