Confuses import of Coq

Question

Can someone please tell me about the differences between

• Require Name.
• Require Import Name.
• Import Name

?

Answer 1

• Require : load an external library (usually from the standard library or user-contribs/ folder);
• Import : imports names in the module. For example, if you have a function f in module M by doing Import M. , you would need to enter f instead of Mf ;
• Require Import : Performs both Require and Import .