add 'notypeclasses apply' tactic

notypeclasses apply is like notypeclasses refine except that it adds sufficiently many underscores automatically, thus making it less fragile to use.

This version adds underscores until the term is not a function any more. That is less smart than apply/apply:, so maybe we should pick a different name? We could also try applying after each _, though that could be slow if unification goes wrong.

@msammler I found a case in the bitvector lib that seems like it could use the new tactic. I hope it is covered by tests, otherwise I am not sure if it still works.^^

Fixes #220 (closed)

stdpp/tactics.v

@@ -736,6 +736,12 @@ Tactic Notation "ospecialize" "*" uconstr(p) :=
       pose proof p as H'; clear H; rename H' into H
   )).
 
+(** 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). *)
+Tactic Notation "notypeclasses" "apply" uconstr(p) :=
+  opose_specialize_foralls_core p () ltac:(fun p => notypeclasses refine p).
+
 (** The block definitions are taken from [Coq.Program.Equality] and can be used
 by tactics to separate their goal from hypotheses they generalize over. *)
 Definition block {A : Type} (a : A) := a.