diff --git a/stdpp/tactics.v b/stdpp/tactics.v index dd2c1598960987c19be0eff17859e369102a0bfb..9bc05c26d1b573371441f8853254397e338a0477 100644 --- a/stdpp/tactics.v +++ b/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).