Allow open terms in "apply ->" and "apply <-" (fix coq#18177).

In particular, these tactics can now be used with a symbol that has some
implicit arguments.

doc/changelog/05-Ltac-language/18946-apply.rst

@@ -0,0 +1,7 @@
+- **Changed:**
+  When used with a direction :n:`->` or :n:`<-`, :tacn:`apply` now accepts an open term,
+  assuming its holes can be inferred during application, as was already the case for plain
+  :tacn:`apply`
+  (`#18946 <https://github.com/coq/coq/pull/18946>`_,
+  fixes `#18177 <https://github.com/coq/coq/issues/18177>`_,
+  by Guillaume Melquiond).

test-suite/bugs/bug_18177.v

@@ -0,0 +1,9 @@
+From Coq Require Import PeanoNat.
+
+Arguments Nat.succ_lt_mono {n m}.
+
+Lemma bar (n m : nat) : n < m -> S n < S m.
+Proof.
+  intros H.
+  now apply -> Nat.succ_lt_mono.
+Qed.

theories/Init/Tactics.v

@@ -140,16 +140,16 @@ let H := fresh in
   pose proof lemma as H;
   find_equiv H; [todo H; clear H | .. ].
 
-Tactic Notation "apply" "->" constr(lemma) :=
+Tactic Notation "apply" "->" open_constr(lemma) :=
 bapply lemma ltac:(fun H => destruct H as [H _]; apply H).
 
-Tactic Notation "apply" "<-" constr(lemma) :=
+Tactic Notation "apply" "<-" open_constr(lemma) :=
 bapply lemma ltac:(fun H => destruct H as [_ H]; apply H).
 
-Tactic Notation "apply" "->" constr(lemma) "in" hyp(J) :=
+Tactic Notation "apply" "->" open_constr(lemma) "in" hyp(J) :=
 bapply lemma ltac:(fun H => destruct H as [H _]; apply H in J).
 
-Tactic Notation "apply" "<-" constr(lemma) "in" hyp(J) :=
+Tactic Notation "apply" "<-" open_constr(lemma) "in" hyp(J) :=
 bapply lemma ltac:(fun H => destruct H as [_ H]; apply H in J).
 
 (** An experimental tactic simpler than auto that is useful for ending