Skip to content
Snippets Groups Projects
Commit 233acb0d authored by Ralf Jung's avatar Ralf Jung
Browse files

notypeclasses apply: fix comment

parent 96ef0cd6
No related branches found
No related tags found
1 merge request!585notypeclasses apply: fix comment
Pipeline #115792 passed
......@@ -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).
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment