diff options
| -rw-r--r-- | parsing/pcoq.ml | 2 | ||||
| -rw-r--r-- | parsing/pcoq.mli | 2 | ||||
| -rw-r--r-- | plugins/ltac/g_tactic.mlg | 2 | ||||
| -rw-r--r-- | toplevel/g_toplevel.mlg | 2 | ||||
| -rw-r--r-- | user-contrib/Ltac2/g_ltac2.mlg | 2 |
5 files changed, 5 insertions, 5 deletions
diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml index 4b42c59d54..d1a6e0eda2 100644 --- a/parsing/pcoq.ml +++ b/parsing/pcoq.ml @@ -165,7 +165,7 @@ struct | Tok.IDENT ident when not (List.mem_f String.equal ident idents) -> Some (n + 1) | _ -> None - let lk_int tok n strm = match stream_nth n strm with + let lk_nat tok n strm = match stream_nth n strm with | Tok.NUMERAL { NumTok.int = _; frac = ""; exp = "" } -> Some (n + 1) | _ -> None 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 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) *) 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 } diff --git a/user-contrib/Ltac2/g_ltac2.mlg b/user-contrib/Ltac2/g_ltac2.mlg index ad6949b899..a0984aa2a9 100644 --- a/user-contrib/Ltac2/g_ltac2.mlg +++ b/user-contrib/Ltac2/g_ltac2.mlg @@ -27,7 +27,7 @@ let lk_ident_or_anti = let test_lpar_idnum_coloneq = let open Pcoq.Lookahead in to_entry "test_lpar_idnum_coloneq" begin - lk_kw "(" >> (lk_ident_or_anti <+> lk_int) >> lk_kw ":=" + lk_kw "(" >> (lk_ident_or_anti <+> lk_nat) >> lk_kw ":=" end (* lookahead for (x:t), (?x:t) *) |