From 0b969ed83ee9db57c748a23e1e7f1da722e46e42 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Wed, 25 Oct 2023 18:12:48 +0200 Subject: [PATCH] [fixup 8.16] Stream module missing in 8.16 --- controller/rq_goals.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/controller/rq_goals.ml b/controller/rq_goals.ml index 35c7027e..9ff66675 100644 --- a/controller/rq_goals.ml +++ b/controller/rq_goals.ml @@ -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 = _ }