title: Coq: why do I need to manually unfold a value even though it has a `Hint Unfold` on it?
body: <p>I've come up with the following toy proof script:</p>
  
  <pre><code>Inductive myType : Type :=
  | c : unit -&gt; myType.
  
  Inductive myProp : myType -&gt; Type :=
  | d : forall t, myProp (c t).
  Hint Constructors myProp.
  
  Definition myValue : myType := c tt.
  Hint Unfold myValue.
  
  Example test: myProp myValue.
  Proof.
    auto 1000. (* does nothing *)
    unfold myValue.
    trivial.
  Qed.
  </code></pre>
  
  <p>Why do I need to manually unfold <code>myValue</code> here? Shouldn't the hint suffice?</p>