From 233acb0d683e544e0b7e131f63c4ef5c39d3d148 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 6 Feb 2025 16:41:29 +0100
Subject: [PATCH] notypeclasses apply: fix comment

---
 stdpp/tactics.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/stdpp/tactics.v b/stdpp/tactics.v
index dd2c1598..9bc05c26 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).
 
-- 
GitLab