title: Unable to locate library
body: <p>The same Linux command succeeds in one environment while it fails in another:</p>
  
  <pre><code>$ coqtop -lv test.v -I Lib
  </code></pre>
  
  <p>The failure I am getting is under Debian stretch and Coq v8.5</p>
  
  <pre><code>$ uname -a
  Linux front 4.8.0-1-amd64 #1 SMP Debian 4.8.7-1 (2016-11-13) x86_64 GNU/Linux
  
  $ coqtop -v
  The Coq Proof Assistant, version 8.5 (June 2016)
  compiled on Jun 9 2016 12:4:46 with OCaml 4.02.3
  </code></pre>
  
  <p>and the error message I am getting is:</p>
  
  <pre><code>Welcome to Coq 8.5 (June 2016)
  Require Import libtest.
  Error during initialization:
  File "/home/user/dev/coq/test.v", line 1, characters 15-22:
  Error: Unable to locate library libtest.
  </code></pre>
  
  <p>The environment under which the same command relating to the same source succeeds is:</p>
  
  <pre><code>$ uname -a 
  Linux back 3.16.0-4-amd64 #1 SMP Debian 3.16.36-1+deb8u2 (2016-10-19)x86_64 GNU/...
  
  $ coqtop
  The Coq Proof Assistant, version 8.4pl4 (July 2014)
  compiled on Jul 27 2014 13:34:24 with OCaml 4.01.0
  </code></pre>
  
  <p>The successful outcome is as follows:</p>
  
  <pre><code>Welcome to Coq 8.4pl4 (July 2014)
  Require Import libtest.
  
  Coq &lt;     
  </code></pre>
  
  <p>So I am trying to figure out what is going on, hoping to get an answer from
  <a href="https://stackoverflow.com/questions/16202666/coqide-cant-load-modules-from-same-folder">this post</a> but to no avail.</p>
  
  <p>For the sake of this question, I have reduced the source code to the simplest:</p>
  
  <p><strong>test.v</strong></p>
  
  <pre><code>Require Import libtest.
  </code></pre>
  
  <p><strong>Lib/libtest.v</strong></p>
  
  <pre><code>&lt;empty file&gt;
  </code></pre>
  
  <p>In case this matters I have recompiled the (empty) library file <code>libtest.v</code> in each environment.</p>
  
  <pre><code>$ cd Lib
  $ coqc libtest.v
  $ cd ..
  </code></pre>
  
  <p>Any help is gratefully appreciated.</p>