This page lists a collection of recurrent questions.
- CoqIDE is unable to import modules such as TacticsL8 and Maps. How can I import them?
A: It might help to add to the loadpath the directory where the modules are. You can do this by adding to your Coq file the command Add LoadPath "PATH", where PATH is the directory. For example: Add LoadPath "C:\Documents\LP"