Using arrows in coqtop

Using Coq
1

I can not use arrows in coqtop, as one would expect in any repl. For example, in OCaml’s utop, up arrow allows to copy previously executed code. However, in coqtop, the up arrow prints the following text:

Coq < ^[[A

Also, after making a mistake while typing, I do not know how to navigate back, using the left, without deleting previously written text

2

coqtop is not meant for direct usage, it mostly exists for Proof General and for testing.
If you must use coqtop directly you can call it through GitHub - hanslub42/rlwrap: A readline wrapper to get GNU readline features.