The Coq mailing list

[Thomas Geffroy <tgeffroy AT enseirb-matmeca.fr>]

Hi all,


I saw few methods to import a module.

I generally use "Add Rec LoadPath "path" as Name_File" with a file Name_file.vo in path/ and then i use Require Import Name_File. Sometimes it works, sometimes not.
"The file path/File_Name.vo contains library
File_Name and not library File_Name.File_Name"

What is the right way to import a module ?


Thanks

Thomas Geffroy