Curry universally quantified function

I am trying to write a tactic for currying functions, including universally quantified functions.

Require Import Coq.Program.Tactics.

Definition curry1 := forall A B C, (A /\ B -> C) -> (A -> B -> C).
Definition curry2 := forall A B, (forall C, A /\ B -> C) -> (forall C, A -> B -> C).
Definition curry3 := forall A, (forall B C, A /\ B -> C) -> (forall B C, A -> B -> C).
(* etc. *)

Ltac curry H :=
  let T := type of H in
  match T with
  | _ /\ _ -> _ =>
    replace_hyp H (fun H1 => fun H2 => H (conj H1 H2))
  | forall x, ?P x =>
    fail 1 "not implemented"
  | _ =>
    fail 1 "not a curried function"
  end.

Example ex1 : curry1.
Proof.
  intros A B C H.
  curry H.
  assumption.
Qed.

Example ex2 : curry2.
Proof.
  intros A B H.
  Fail curry H. (* Tactic failure: not a curried function. *)
  Fail replace_hyp H (fun H1 => let H2 := H H1 in ltac:(curry H2)). (* Cannot infer an existential variable of type "Type" in environment: [...] *)
Abort.

How can I extend my curry tactic to handle universally quantified functions?