diff --git a/CHANGELOG.md b/CHANGELOG.md
index 0399e0d88846ed54c2db3e1e33c52b40b297a1ab..9a9c58eb7d687d07bd956c6b37c40f17e99b6be7 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -53,6 +53,7 @@ Coq 8.8 and 8.9 are no longer supported.
   are used for `A → B1` and `A → B2` variants of `A ↔ B1 ∧ B2` lemmas.
 - Rename `Forall_Forall2` → `Forall_Forall2_diag` to be consistent with the
   names for big operators in Iris.
+- Add `eunify` tactic that lifts Coq's `unify` tactic to `open_constr`.
 
 The following `sed` script should perform most of the renaming
 (on macOS, replace `sed` by `gsed`, installed via e.g. `brew install gnu-sed`):
diff --git a/tests/eunify.ref b/tests/eunify.ref
new file mode 100644
index 0000000000000000000000000000000000000000..2dc91ac73d672c3052e9272658799c11c3fec75f
--- /dev/null
+++ b/tests/eunify.ref
@@ -0,0 +1,13 @@
+"eunify_test"
+     : string
+The command has indeed failed with message:
+No matching clauses for match.
+((fix add (n m : nat) {struct n} : nat :=
+    match n with
+    | 0 => m
+    | S p => S (add p m)
+    end) x y)
+"eunify_test_evars"
+     : string
+The command has indeed failed with message:
+No matching clauses for match.
diff --git a/tests/eunify.v b/tests/eunify.v
new file mode 100644
index 0000000000000000000000000000000000000000..c12cc61862ee34ff378f3f5f5142eb61d0210f32
--- /dev/null
+++ b/tests/eunify.v
@@ -0,0 +1,44 @@
+From stdpp Require Import tactics strings.
+
+Check "eunify_test".
+Lemma eunify_test : ∀ x y, 0 < S x + y.
+Proof.
+  intros x y.
+  (* Test that Ltac matching fails, otherwise this test is pointless *)
+  Fail
+    match goal with
+    | |- 0 < S _ => idtac
+    end.
+  (* [eunify] succeeds *)
+  match goal with
+  | |- 0 < ?x => eunify x (S _)
+  end.
+  match goal with
+  | |- 0 < ?x => let y := open_constr:(_) in eunify x (S y); idtac y
+  end.
+  lia.
+Qed.
+
+Check "eunify_test_evars".
+Lemma eunify_test_evars : ∃ x y, 0 < S x + y.
+Proof.
+  eexists _, _.
+  (* Test that Ltac matching fails, otherwise this test is pointless *)
+  Fail
+    match goal with
+    | |- 0 < S _ => idtac
+    end.
+  (* [eunify] succeeds even if the goal contains evars *)
+  match goal with
+  | |- 0 < ?x => eunify x (S _)
+  end.
+  (* Let's try to use [eunify] to instantiate the first evar *)
+  match goal with
+  | |- 0 < ?x => eunify x (1 + _)
+  end.
+  (* And the other evar *)
+  match goal with
+  | |- 0 < ?x => eunify x 2
+  end.
+  lia.
+Qed.
\ No newline at end of file
diff --git a/theories/tactics.v b/theories/tactics.v
index 54e8189ca0462fa1b1fe1325117bf8e9c26f9d23..bc3a43b24cd592d77870835b5428103a6815e05b 100644
--- a/theories/tactics.v
+++ b/theories/tactics.v
@@ -214,6 +214,16 @@ does the converse. *)
 Ltac var_eq x1 x2 := match x1 with x2 => idtac | _ => fail 1 end.
 Ltac var_neq x1 x2 := match x1 with x2 => fail 1 | _ => idtac end.
 
+(** The tactic [eunify x y] succeeds if [x] and [y] can be unified, and fails
+otherwise. If it succeeds, it will instantiate necessary evars in [x] and [y].
+
+Contrary to Coq's standard [unify] tactic, which uses [constr] for the arguments
+[x] and [y], [eunify] uses [open_constr] so that one can use holes (i.e., [_]s).
+For example, it allows one to write [eunify x (S _)], which will test if [x]
+unifies a successor. *)
+Tactic Notation "eunify" open_constr(x) open_constr(y) :=
+  unify x y.
+
 (** Operational type class projections in recursive calls are not folded back
 appropriately by [simpl]. The tactic [csimpl] uses the [fold_classes] tactics
 to refold recursive calls of [fmap], [mbind], [omap] and [alter]. A