Cannot backtrack over Require Import with Go to Point

[tchajed]

If you process a Require Import, you can backtrack over it with Step Backward, but not with Go to Point.

[Durbatuluk1701]

I think I see what you are saying, something like:

... (no valid command here that could be interpreted to) ...
|
Require Import X.
...

Go to point (where | is cursor) if the Require Import X. statement has already been processed does not backtrack it.

Can you confirm that if there is a valid command above the Require Import you can backtrack with Go to Point, as that is the behavior that I am seeing.

[tchajed]

I generally have a comment above Require Import, if anything - for Coq to behave sensibly you want to start with all the Require statements.

When I put a Check nat. above my Require Import I can backtrack to the beginning of the Require Import but not before Check nat (using Go to Point specifically).

[Durbatuluk1701]

So I think ultimately the desired behavior is to be able to backtrack to before the very initial command in a file via Go to Point?

[tchajed]

That is what I would want, yes.

I should mention that this issue is low priority for me, since if I really need it I use Coq: Reset. However, sometimes reloading a dependency that has changed is useful and it's nice to use backtracking for that.