Ali Caglayan (Feb 16 2022 at 11:37): Ali Caglayan (Feb 16 2022 at 11:37):Is there a command that prints all the commands that came before? Using coqtop
Gaëtan Gilbert (Feb 16 2022 at 11:38):https://github.com/coq/coq/commit/6a5dcbbfea1af0308a4d49e7c5bcea26d74a739d
Gaëtan Gilbert (Feb 16 2022 at 11:39):tldr use a text editor
Paolo Giarrusso (Feb 16 2022 at 11:39):if you wanted prompt conveniences there's rlwrap but I agree
Gaëtan Gilbert (Feb 16 2022 at 11:54):the coqtop specific commands are in https://github.com/coq/coq/blob/master/toplevel/g_toplevel.mlg btw
Emilio Jesús Gallego Arias (Feb 16 2022 at 12:31):Now that we have dune I'm all for vendoring some readline like library and linking to coqtop
Emilio Jesús Gallego Arias (Feb 16 2022 at 12:31):that's a nice hacktahon project
Emilio Jesús Gallego Arias (Feb 16 2022 at 12:31):I have a pr to used utop on Drop too
Emilio Jesús Gallego Arias (Feb 16 2022 at 12:31):I'll be happy to supervise it
Last updated: Jun 05 2023 at 09:01 UTC