import module edit

[nomeata]

I think we could have much prettier output with a

import module Foo

edits, which has these effects:

• Require Foo. turns into Require Import Foo.
• No Import Foo.Notations.
• All uses of names in Foo are printed unqualified.

Because it is opt-in, it is now the responsibility of the user to ensure that this does not lead to name clashes … or are the dangers of unnoticed shadowing too big to even offer that feature?

[sweirich]

Let's try it out.