XXX "is bound to a notation that does not denote a reference" during unfold in Coq?

Question

I am working on an example given here:

Notation step_normal_form := (normal_form step).
Definition stuck (t:tm) : Prop :=
  step_normal_form t /\ ~ value t.

Example some_term_is_stuck :
  exists t, stuck t.

and I am having trouble unfold-ing the definition step_normal_form at step 1 (Coq 8.4pl6). I can Check its contents in CoqIDE:

normal_form
     : relation ?23 -> ?23 -> Prop
value
 : tm -> Prop

But when I unfold step_normal_form:

Example some_term_is_stuck :
  exists t, stuck t.
Proof.
  unfold stuck. unfold step_normal_form.

I get an error:

Error: step_normal_form is bound to a notation that does not denote a reference.

Does anyone know why this happens and how to fix it?

BTW, I tried to work around this by doing the unfold manually and redefining:

Definition stuck' (t:tm) : Prop :=
  normal_form step t /\ ~ value t.

and use stuck' instead. But Coq seems to automatically fold the content of stuck' into step_normal_form and then refuse to unfold it, giving the same error.

Answer 1

Since step_normal_form is just notation for (normal_form step) you could just do unfold normal_form.

Sometimes notations and pretty-printing hides what's really there. Use Set Printing All. to make Coq print the term in clear.