Merge PR #14089: unify for Ltac2

Reviewed-by: ppedrot

7 files changed, 46 insertions, 0 deletions

diff --git a/doc/changelog/04-tactics/14089-ltac2_unify.rst b/doc/changelog/04-tactics/14089-ltac2_unify.rst
new file mode 100644
index 0000000000..5887781db9
--- /dev/null
+++ b/doc/changelog/04-tactics/14089-ltac2_unify.rst
@@ -0,0 +1,5 @@
+- **Added:**
+  Ltac2 now has a `unify` tactic
+  (`#14089 <https://github.com/coq/coq/pull/14089>`_,
+  fixes `#14083 <https://github.com/coq/coq/issues/14083>`_,
+  by Samuel Gruetter).
diff --git a/test-suite/ltac2/std_tactics.v b/test-suite/ltac2/std_tactics.v
new file mode 100644
index 0000000000..39b620a6ac
--- /dev/null
+++ b/test-suite/ltac2/std_tactics.v
@@ -0,0 +1,29 @@
+Require Import Ltac2.Ltac2.
+
+Axiom f: nat -> nat.
+Definition g := f.
+
+Axiom Foo1: nat -> Prop.
+Axiom Foo2: nat -> Prop.
+Axiom Impl: forall n: nat, Foo1 (f n) -> Foo2 (f n).
+
+Create HintDb foo discriminated.
+#[export] Hint Constants Opaque : foo.
+#[export] Hint Resolve Impl : foo.
+
+Goal forall x, Foo1 (f x) -> Foo2 (g x).
+Proof.
+  auto with foo.
+  #[export] Hint Transparent g : foo.
+  auto with foo.
+Qed.
+
+Goal forall (x: nat), exists y, f x = g y.
+Proof.
+  intros.
+  eexists.
+  unify f g.
+  lazy_match! goal with
+  | [ |- ?a ?b = ?rhs ] => unify ($a $b) $rhs
+  end.
+Abort.
diff --git a/user-contrib/Ltac2/Notations.v b/user-contrib/Ltac2/Notations.v
index 931d753521..6ddad8f1c9 100644
--- a/user-contrib/Ltac2/Notations.v
+++ b/user-contrib/Ltac2/Notations.v
@@ -593,6 +593,8 @@ Ltac2 Notation "typeclasses_eauto" "bfs" n(opt(tactic(0)))
 
 Ltac2 Notation typeclasses_eauto := typeclasses_eauto.
 
+Ltac2 Notation "unify" x(constr) y(constr) := Std.unify x y.
+
 (** Congruence *)
 
 Ltac2 f_equal0 () := ltac1:(f_equal).
diff --git a/user-contrib/Ltac2/Std.v b/user-contrib/Ltac2/Std.v
index b69a95faf3..3675df9f75 100644
--- a/user-contrib/Ltac2/Std.v
+++ b/user-contrib/Ltac2/Std.v
@@ -259,3 +259,5 @@ Ltac2 @ external new_auto : debug -> int option -> (unit -> constr) list -> iden
 Ltac2 @ external eauto : debug -> int option -> int option -> (unit -> constr) list -> ident list option -> unit := "ltac2" "tac_eauto".
 
 Ltac2 @ external typeclasses_eauto : strategy option -> int option -> ident list option -> unit := "ltac2" "tac_typeclasses_eauto".
+
+Ltac2 @ external unify : constr -> constr -> unit := "ltac2" "tac_unify".
diff --git a/user-contrib/Ltac2/tac2stdlib.ml b/user-contrib/Ltac2/tac2stdlib.ml
index 895b6d3975..c7dfb3e69e 100644
--- a/user-contrib/Ltac2/tac2stdlib.ml
+++ b/user-contrib/Ltac2/tac2stdlib.ml
@@ -572,3 +572,7 @@ end
 let () = define_prim3 "tac_typeclasses_eauto" (option strategy) (option int) (option (list ident)) begin fun str n dbs ->
   Tac2tactics.typeclasses_eauto str n dbs
 end
+
+let () = define_prim2 "tac_unify" constr constr begin fun x y ->
+  Tac2tactics.unify x y
+end
diff --git a/user-contrib/Ltac2/tac2tactics.ml b/user-contrib/Ltac2/tac2tactics.ml
index 54f5a2cf68..a30f6e7945 100644
--- a/user-contrib/Ltac2/tac2tactics.ml
+++ b/user-contrib/Ltac2/tac2tactics.ml
@@ -414,6 +414,8 @@ let typeclasses_eauto strategy depth dbs =
   in
   Class_tactics.typeclasses_eauto ~only_classes ?strategy ~depth dbs
 
+let unify x y = Tactics.unify x y
+
 (** Inversion *)
 
 let inversion knd arg pat ids =
diff --git a/user-contrib/Ltac2/tac2tactics.mli b/user-contrib/Ltac2/tac2tactics.mli
index f63f7e722a..47a3fd5987 100644
--- a/user-contrib/Ltac2/tac2tactics.mli
+++ b/user-contrib/Ltac2/tac2tactics.mli
@@ -119,6 +119,8 @@ val eauto : Hints.debug -> int option -> int option -> constr thunk list ->
 val typeclasses_eauto : Class_tactics.search_strategy option -> int option ->
   Id.t list option -> unit Proofview.tactic
 
+val unify : constr -> constr -> unit tactic
+
 val inversion : Inv.inversion_kind -> destruction_arg -> intro_pattern option -> Id.t list option -> unit tactic
 
 val contradiction : constr_with_bindings option -> unit tactic