title: Coq + Emacs? ``Check`` can't see what is defined in the source file
body: <p>So I am playing with <code>Coq</code> using <code>Emacs</code> as the IDE. Both <code>proof-general</code> and <code>company-coq</code> are installed and load correctly.</p>
  <p>Then I open dummy <code>whatever_name.v</code> file and define recursive function using the <code>Fixpoint</code> keyword.</p>
  <p>Then I run <code>coq-Check</code> on it and get:</p>
  <blockquote>
  <p>&gt; Check addnm .</p>
  <p>Error: The reference addnm was not found in the current environment.</p>
  </blockquote>
  <p>However, for example, <code>Inductive unit : Set := tt.</code> works perfectly well.</p>
  <p>What am I doing wrong?</p>
  <p><a href="https://i.stack.imgur.com/5Pa7a.png" rel="nofollow noreferrer"><img src="https://i.stack.imgur.com/5Pa7a.png" alt="enter image description here" /></a></p>