Pattern matching over goals

Pattern matching over goals is implemented by the match%rocq goal with syntax:

Camltac Module My_tauto := ocaml:{{
  let run () =
    let* () = intros [] in
    let open Ltac2 in
    repeat begin match%rocq goal with
    | { h = _ :: {| _ -> ?b |} }, {| ?b |} ->
       let* env in
       let h = Control.hyp env h in
       apply [term h]
    | _, {| _ \/ _ |} ->
       Control.plus (left ()) (fun _ -> right ())
    | _, _ ->
       assumption ()
    end
}}.
unused variable b.


Goal forall A B C, (C -> A) -> C -> A \/ B.
forall (A B : Prop) (C : Type), (C -> A) -> C -> A \/ B
Proof.
forall (A B : Prop) (C : Type), (C -> A) -> C -> A \/ B
  ocaml:(My_tauto.run ()).
Qed.