Non-FFI file with imports generates code that triggers Coq warnings

[RalfJung]

Goose on this example produces code like this

From Perennial.goose_lang Require Import prelude.
Section code.
Context `{ext_ty: ext_types}.
Local Coercion Var' s: expr := Var s.

From Goose Require github_com.goose_lang.std.

This generates a Coq warning about Require inside Section.

This seems a bit annoying to fix since I think the Require std is part of the Decls []Decl in a File that also contain all the actual definitions. But we want to split this into stuff that is put outside the section and stuff that is put inside the section. @tchajed @upamanyu any good ideas for how to do that?

[tchajed]

I think a File really shouldn't put requires into Decls, they should instead be in a separate field dedicated to imports. A hack would be to extract them by looking for ImportDecls but that just seems messy.

[RalfJung]

filterImports actually already walks over all decls and dispatches on the coq.ImportDecl type...

[tchajed]

Ah so that's the actual reason why the imports even end up together rather than scattered randomly through the file (right before they're needed). Well I guess with this cleanup we could get rid of that, but actually the bug could be fixed within interface.go itself probably.