What is the right proof term so that the ssreflect tutorial work with the exact: hAiB example?

Question

I was going through the tutorial https://hal.inria.fr/inria-00407778/document for ssreflect and they have the proof:

Variables A B C : Prop.
Hypotheses (hAiBiC : A -> B -> C) (hAiB : A -> B) (hA : A).
Lemma HilbertS2 : 
  C. 
Proof. 
  apply: hAiBiC; first by apply: hA. 
  exact: hAiB. 
Qed.

but it doesn't actually work since the goal is

B

which puzzled me...what is this not working because the coq version changed? Or perhaps something else? What was the exact argument supposed to be anyway?

---

I think I do understand what the exact argument does. It completes the current subgoal by making sure the proof term (program) given has the type of the current goal. e.g.

Theorem add_easy_induct_1_exact:
forall n:nat,
  n + 0 = n.
Proof.
  exact (fun n : nat =>
nat_ind (fun n0 : nat => n0 + 0 = n0) eq_refl
   (fun (n' : nat) (IH : n' + 0 = n') =>
    eq_ind_r (fun n0 : nat => S n0 = S n') eq_refl IH) n).
Qed.

for the proof of addition's commutativity.

---

Module ssreflect1.

(* Require Import ssreflect ssrbool eqtype ssrnat. *)
From Coq Require Import ssreflect ssrfun ssrbool.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Theorem three_is_three:
  3 = 3.
Proof. by []. Qed.

(* 
https://stackoverflow.com/questions/71388591/what-does-apply-tactic-on-its-own-do-in-coq-i-e-without-specifying-a-rul
*)
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 [].
(* move: hAiB.
apply. *)
by apply: hAiB.
(* apply: hAiB.
by [].dd *)
Qed.

Variables A B C : Prop.
Hypotheses (hAiBiC : A -> B -> C) (hAiB : A -> B) (hA : A).
Lemma HilbertS2 : 
  C. 
Proof. 
  apply: hAiBiC; first by apply: hA. 
  exact: hAiB. 
Qed.

Lemma HilbertS2 : 
  C. 
Proof. 
  (* apply: hAiBiC; first by apply: hA. *)
  apply: hAiBiC. (* usually we think of : as pushing to the goal stack, so match c with conclusion in
  selected hypothesis hAiBiC and push the replacement, so put A & B in local context. *)
  by apply: hA. (* discharges A *)
  exact: hAiB.

End ssreflect1.

full script I was using. Why does that not put the hypothesis in the local context?