F* has a special qualifier for KreMLin [@"substitute"] that fstar-mode doesn't recognize, so that advancing processes any definitions with this qualifier:
module Interactive_advance_substitute
(* fstar-subp-advance-next here... *)
let a = 1
[@"substitute"] let b = 2
(* ... goes here *)
This is low priority, and I'm not sure if this type of qualifier will stick around in F*.
The fix would be to refine the predicate that's used for picking headers to start on. Currently it checks for preceding blanks and being outside of a comment.
F* has a special qualifier for KreMLin
[@"substitute"]
that fstar-mode doesn't recognize, so that advancing processes any definitions with this qualifier:This is low priority, and I'm not sure if this type of qualifier will stick around in F*.