notypeclasses apply: fix comment

The implementation actually uses eval hnf, so it is not purely syntactic.

I don't know what behavior we want, but clearly docs and implementation should match... and for the o* tactics, unfolding seems to work better; e.g. we have existing uses of oinversion on statements of the form ... → not _ that would otherwise break.

stdpp/tactics.v

@@ -738,7 +738,7 @@ Tactic Notation "ospecialize" "*" uconstr(p) :=
 
 (** Tactic that works like [notypeclasses refine] but automatically determines
 the right number of [_]. This is *not* goal-directed, it will add [_] until the
-given term no longer has a function type (determined via syntactic matching). *)
+given term no longer has a function type (determined via [eval hnf]). *)
 Tactic Notation "notypeclasses" "apply" uconstr(p) :=
   opose_specialize_foralls_core p () ltac:(fun p => notypeclasses refine p).