What does `apply.` tactic on it's own do in Coq -- i.e. without specifying a rule or hypothesis to unify the goal's conclusion with?

Question

I think I understand the main idea of the apply tactic but I can't figure out what it does in this case:

Lemma HilbertS : 
  forall A B C : Prop, 
    (A -> B -> C) -> (A -> B) -> A -> C.
  (* A ->(B -> C)*)
Proof.
  move=> A B C. (* since props A B C are the 1st things in the assumption stack, this pops them and puts them in the local context, note using the same name as the proposition name.*)
  move=> hAiBiC hAiB hA. (* pops the first 3 premises from the hypothesis stack with those names into the local context *)
  move: hAiBiC. (* put hAiBiC tactic back *)
apply.
by [].
by apply: hAiB.
Qed.

I know that the apply tactic receives a hypothesis and matches the conclusion of the hypothesis with conclusion of the subgoal (I assume the current focused subgoal) and if they unify then uses the substitution from the unification to update the premises of the hypothesis as the new subgoal(s). See appendix for details.

However, in the HilbertS proof I gave I can't figure out what apply. is actually doing and the docs from the regular tactics in coq and the ssreflex in coq aren't helping.

Note the proof state is:

A, B, C: Prop
hAiB: A -> B
hA: A
====
1/1
(A -> B -> C) -> C

What is apply. doing here if the hypothesis is not even being select? I assume it's unify with something but C is not in any of the hypothesis in the local context so it's really confusing me what it's even unifying with. Basically what is apply. doing here -- especially without a hypothesis/term argument givent o the tactic apply (in SSReflect)?

---

Appendix explaining my understanding of apply

(* 
https://pjreddie.com/coq-tactics/#apply 

Usually an apply in Isabelle matches the rule's conclusion with the subgoal's 
conclusion, unifies them and if them match then replaces the rules hypothesis
as the things to be proven given the substitution
e.g.
rule1 A1 => A2 => A
subgoal: B1 => B2 => C
apply rule rule. (* replace C with A1 A1 to be proven with the right subtitution*)

sig = Unify(A, C)

new subgoals:
sig(B1) => sig(B2) => sig(A1)
sig(B1) => sig(B2) => sig(A2)

note: notation: proof_state = <local_context, goals>
*)
Lemma modus_ponens:
  forall p q : Prop, 
    (p -> q) -> p -> q.
Proof.
  intros. (*  <H: p -> q, H0: p, q> *)
  apply H. (* matches H cocnlusion q with goal q, replaces p to be proven now *)
  assumption. (* goal p is in the assumption in the local context, so discharge it *)
Qed.

From Coq Require Import ssreflect ssrfun ssrbool.
Lemma modus_ponens':
  forall p q : Prop, 
    (p -> q) -> p -> q.
Proof.
  move=> p q p_implies_q p_fact. (* <..., p_fact: p, p_implies)q: p->q, goal=q>*)
  apply: p_implies_q.
  assumption.
Qed.

Answer 1

The SSReflect documentation you linked says what it does:

In its defective form, this tactic is a synonym for:

intro top; first [refine top | refine (top _) | refine (top _ _) | …]; clear top.

where top is a fresh name, and the sequence of refine tactics tries to catch the appropriate number of wildcards to be inserted. Note that this use of the refine tactic implies that the tactic tries to match the goal up to expansion of constants and evaluation of subterms.

I.e. apply. takes a goal of the form A -> R and, in sequence, tries to unify (roughly) A = R, A = H1 -> R, A = H1 -> H2 -> R, etc. until it gets a unification for some H1, ..., Hn (so the goal looks like (H1 -> ... -> Hn -> R) -> R). Then it turns this into subgoals H1, ..., Hn by using the H1 -> ... -> Hn -> R hypothesis to combine the subgoals into the R conclusion. (The actual behavior is more general than this, since it should be able to handle dependent products too.) Or, in short,

apply.

is basically

intros H. apply H; clear H.