Skip to content

Commit

Permalink
[fixup 8.16] Stream module missing in 8.16
Browse files Browse the repository at this point in the history
  • Loading branch information
ejgallego committed Oct 25, 2023
1 parent 03ce297 commit 0b969ed
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion controller/rq_goals.ml
Original file line number Diff line number Diff line change
Expand Up @@ -40,7 +40,7 @@ let pp ~pp_format pp =
we should tune whether we cache the results; we try this for now. *)
let parse_and_execute_in tac st =
(* Parse tac, loc==FIXME *)
let str = Gramlib.Stream.of_string tac in
let str = Stream.of_string tac in
let str = Coq.Parsing.Parsable.make ?loc:None str in
match Coq.Parsing.parse ~st str with
| Coq.Protect.E.{ r = Interrupted; feedback = _ }
Expand Down

0 comments on commit 0b969ed

Please sign in to comment.