Currently, M-. (fstar-jump-to-definition) jumps to the fst of the module, when we do it over an open ModuleName, even if an fsti exists. I think it would be better if it were to jump over to the fsti and rely on a user to press C-c C-a (fstar-visit-interface-or-implementation) if need be to jump over to the implementation.

Not sure if this is something that needs to be fixed on the compiler side or on the fstar-mode side, but it would be a nice QoL improvement.