diff options
Diffstat (limited to 'toplevel/coqloop.ml')
| -rw-r--r-- | toplevel/coqloop.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml index d7ede1c2e..7ae15ac10 100644 --- a/toplevel/coqloop.ml +++ b/toplevel/coqloop.ml @@ -23,7 +23,7 @@ type input_buffer = { mutable str : Bytes.t; (* buffer of already read characters *) mutable len : int; (* number of chars in the buffer *) mutable bols : int list; (* offsets in str of beginning of lines *) - mutable tokens : Pcoq.Gram.coq_parsable; (* stream of tokens *) + mutable tokens : Pcoq.Parsable.t; (* stream of tokens *) mutable start : int } (* stream count of the first char of the buffer *) (* Double the size of the buffer. *) @@ -76,7 +76,7 @@ let reset_input_buffer doc ic ibuf = ibuf.str <- Bytes.empty; ibuf.len <- 0; ibuf.bols <- []; - ibuf.tokens <- Pcoq.Gram.parsable (Stream.from (prompt_char doc ic ibuf)); + ibuf.tokens <- Pcoq.Parsable.make (Stream.from (prompt_char doc ic ibuf)); ibuf.start <- 0 (* Functions to print underlined locations from an input buffer. *) @@ -228,7 +228,7 @@ let top_buffer = str = Bytes.empty; len = 0; bols = []; - tokens = Pcoq.Gram.parsable (Stream.of_list []); + tokens = Pcoq.Parsable.make (Stream.of_list []); start = 0 } let set_prompt prompt = @@ -253,7 +253,7 @@ let parse_to_dot = let rec discard_to_dot () = try - Pcoq.Gram.entry_parse parse_to_dot top_buffer.tokens + Pcoq.Entry.parse parse_to_dot top_buffer.tokens with | Token.Error _ | CLexer.Error.E _ -> discard_to_dot () | Stm.End_of_input -> raise Stm.End_of_input |