VERNAC EXTEND should (by default) follow Import rather than Require

[JasonGross]

Require Import Coq.derive.Derive.
Require Equations.Prop.Equations.
Derive foo SuchThat (foo = true) as foo_correct.
(* Error: Syntax error: [ident] or 'for' expected (in [command]). *)

Originally posted by @JasonGross in mattam82/Coq-Equations#515

This is plausibly related to #10146, maybe even to #12575

It was pointed out on Coq call that we may want Require Extraction to be enough to use extraction, so it seems plausible that syntax extensions should be allowed to declare their extensions to be superglobal (i.e., to follow Require), but by default I think it's better to have the vernac syntax extensions follow Import

[SkySkimmer]

This is plausibly related to #10146, maybe even to #12575

It is not, there is no backtracking involved here

[JasonGross]

By related, I meant that it seems impossible to me to fix this issue without also fixing #12575 and probably #10146. Is the backtracking codepath not shared with module closing?