From fb63ec7c10076d156caa43f73bad4f69653862a6 Mon Sep 17 00:00:00 2001
From: Samuel Gruetter
Date: Wed, 7 Apr 2021 21:02:10 -0400
Subject: unify for Ltac2

Fixes #14083
---
 test-suite/ltac2/std_tactics.v     | 34 ++++++++++++++++++++++++++++++++++
 user-contrib/Ltac2/Notations.v     |  2 ++
 user-contrib/Ltac2/Std.v           |  2 ++
 user-contrib/Ltac2/tac2stdlib.ml   |  4 ++++
 user-contrib/Ltac2/tac2tactics.ml  | 14 ++++++++++++++
 user-contrib/Ltac2/tac2tactics.mli |  2 ++
 6 files changed, 58 insertions(+)
 create mode 100644 test-suite/ltac2/std_tactics.v

diff --git a/test-suite/ltac2/std_tactics.v b/test-suite/ltac2/std_tactics.v
new file mode 100644
index 0000000000..a2de3ab763
--- /dev/null
+++ b/test-suite/ltac2/std_tactics.v
@@ -0,0 +1,34 @@
+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.
+  Fail unify f g with core.
+  unify f g with foo.
+  lazy_match! goal with
+  | [ |- ?a ?b = ?rhs ] => unify ($a $b) $rhs with foo
+  end.
+  let dbname := @foo in Std.unify 'f 'g (Some dbname).
+Abort.
diff --git a/user-contrib/Ltac2/Notations.v b/user-contrib/Ltac2/Notations.v
index 931d753521..77531121cb 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) db(opt(seq("with", ident))) := Std.unify x y db.
+
 (** Congruence *)
 
 Ltac2 f_equal0 () := ltac1:(f_equal).
diff --git a/user-contrib/Ltac2/Std.v b/user-contrib/Ltac2/Std.v
index b69a95faf3..17741e563d 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 -> ident option -> unit := "ltac2" "tac_unify".
diff --git a/user-contrib/Ltac2/tac2stdlib.ml b/user-contrib/Ltac2/tac2stdlib.ml
index 895b6d3975..faa0499049 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_prim3 "tac_unify" constr constr (option ident) begin fun x y db ->
+  Tac2tactics.unify x y db
+end
diff --git a/user-contrib/Ltac2/tac2tactics.ml b/user-contrib/Ltac2/tac2tactics.ml
index 54f5a2cf68..de88f2e306 100644
--- a/user-contrib/Ltac2/tac2tactics.ml
+++ b/user-contrib/Ltac2/tac2tactics.ml
@@ -414,6 +414,20 @@ let typeclasses_eauto strategy depth dbs =
   in
   Class_tactics.typeclasses_eauto ~only_classes ?strategy ~depth dbs
 
+let unify x y dbname =
+  match dbname with
+  | None -> Tactics.unify x y
+  | Some name ->
+    let base = Id.to_string name in
+    let table = try Some (Hints.searchtable_map base) with Not_found -> None in
+    match table with
+    | None ->
+      let msg = str "Hint table " ++ str base ++ str " not found" in
+      Tacticals.New.tclZEROMSG msg
+    | Some t ->
+      let state = Hints.Hint_db.transparent_state t in
+      Tactics.unify ~state 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..44041a9e78 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 -> Id.t option -> 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
-- 
cgit v1.2.3


From 807ea5f44ca74c2b2743ed0719e3cbdc46639da7 Mon Sep 17 00:00:00 2001
From: Samuel Gruetter
Date: Thu, 8 Apr 2021 19:41:18 -0400
Subject: remove `with hintdb` variant of Ltac2 `unify`, because

passing one single hintdb is not quite the right API, we should
pass a transparent state instead, but that would require an API
for manipulating hintdbs and transparent states, postponing
---
 test-suite/ltac2/std_tactics.v     |  7 +------
 user-contrib/Ltac2/Notations.v     |  2 +-
 user-contrib/Ltac2/Std.v           |  2 +-
 user-contrib/Ltac2/tac2stdlib.ml   |  4 ++--
 user-contrib/Ltac2/tac2tactics.ml  | 14 +-------------
 user-contrib/Ltac2/tac2tactics.mli |  2 +-
 6 files changed, 7 insertions(+), 24 deletions(-)

diff --git a/test-suite/ltac2/std_tactics.v b/test-suite/ltac2/std_tactics.v
index a2de3ab763..39b620a6ac 100644
--- a/test-suite/ltac2/std_tactics.v
+++ b/test-suite/ltac2/std_tactics.v
@@ -14,9 +14,7 @@ Create HintDb foo discriminated.
 Goal forall x, Foo1 (f x) -> Foo2 (g x).
 Proof.
   auto with foo.
-
   #[export] Hint Transparent g : foo.
-
   auto with foo.
 Qed.
 
@@ -25,10 +23,7 @@ Proof.
   intros.
   eexists.
   unify f g.
-  Fail unify f g with core.
-  unify f g with foo.
   lazy_match! goal with
-  | [ |- ?a ?b = ?rhs ] => unify ($a $b) $rhs with foo
+  | [ |- ?a ?b = ?rhs ] => unify ($a $b) $rhs
   end.
-  let dbname := @foo in Std.unify 'f 'g (Some dbname).
 Abort.
diff --git a/user-contrib/Ltac2/Notations.v b/user-contrib/Ltac2/Notations.v
index 77531121cb..6ddad8f1c9 100644
--- a/user-contrib/Ltac2/Notations.v
+++ b/user-contrib/Ltac2/Notations.v
@@ -593,7 +593,7 @@ Ltac2 Notation "typeclasses_eauto" "bfs" n(opt(tactic(0)))
 
 Ltac2 Notation typeclasses_eauto := typeclasses_eauto.
 
-Ltac2 Notation "unify" x(constr) y(constr) db(opt(seq("with", ident))) := Std.unify x y db.
+Ltac2 Notation "unify" x(constr) y(constr) := Std.unify x y.
 
 (** Congruence *)
 
diff --git a/user-contrib/Ltac2/Std.v b/user-contrib/Ltac2/Std.v
index 17741e563d..3675df9f75 100644
--- a/user-contrib/Ltac2/Std.v
+++ b/user-contrib/Ltac2/Std.v
@@ -260,4 +260,4 @@ Ltac2 @ external eauto : debug -> int option -> int option -> (unit -> constr) l
 
 Ltac2 @ external typeclasses_eauto : strategy option -> int option -> ident list option -> unit := "ltac2" "tac_typeclasses_eauto".
 
-Ltac2 @ external unify : constr -> constr -> ident option -> unit := "ltac2" "tac_unify".
+Ltac2 @ external unify : constr -> constr -> unit := "ltac2" "tac_unify".
diff --git a/user-contrib/Ltac2/tac2stdlib.ml b/user-contrib/Ltac2/tac2stdlib.ml
index faa0499049..c7dfb3e69e 100644
--- a/user-contrib/Ltac2/tac2stdlib.ml
+++ b/user-contrib/Ltac2/tac2stdlib.ml
@@ -573,6 +573,6 @@ let () = define_prim3 "tac_typeclasses_eauto" (option strategy) (option int) (op
   Tac2tactics.typeclasses_eauto str n dbs
 end
 
-let () = define_prim3 "tac_unify" constr constr (option ident) begin fun x y db ->
-  Tac2tactics.unify x y db
+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 de88f2e306..a30f6e7945 100644
--- a/user-contrib/Ltac2/tac2tactics.ml
+++ b/user-contrib/Ltac2/tac2tactics.ml
@@ -414,19 +414,7 @@ let typeclasses_eauto strategy depth dbs =
   in
   Class_tactics.typeclasses_eauto ~only_classes ?strategy ~depth dbs
 
-let unify x y dbname =
-  match dbname with
-  | None -> Tactics.unify x y
-  | Some name ->
-    let base = Id.to_string name in
-    let table = try Some (Hints.searchtable_map base) with Not_found -> None in
-    match table with
-    | None ->
-      let msg = str "Hint table " ++ str base ++ str " not found" in
-      Tacticals.New.tclZEROMSG msg
-    | Some t ->
-      let state = Hints.Hint_db.transparent_state t in
-      Tactics.unify ~state x y
+let unify x y = Tactics.unify x y
 
 (** Inversion *)
 
diff --git a/user-contrib/Ltac2/tac2tactics.mli b/user-contrib/Ltac2/tac2tactics.mli
index 44041a9e78..47a3fd5987 100644
--- a/user-contrib/Ltac2/tac2tactics.mli
+++ b/user-contrib/Ltac2/tac2tactics.mli
@@ -119,7 +119,7 @@ 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 -> Id.t option -> unit tactic
+val unify : constr -> constr -> unit tactic
 
 val inversion : Inv.inversion_kind -> destruction_arg -> intro_pattern option -> Id.t list option -> unit tactic
 
-- 
cgit v1.2.3


From 1dffce05d5b7b26a890a9d0359e54946e661511b Mon Sep 17 00:00:00 2001
From: Samuel Gruetter
Date: Mon, 19 Apr 2021 14:24:50 -0400
Subject: changelog entry for Ltac2 unify

---
 doc/changelog/04-tactics/14089-ltac2_unify.rst | 5 +++++
 1 file changed, 5 insertions(+)
 create mode 100644 doc/changelog/04-tactics/14089-ltac2_unify.rst

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).
-- 
cgit v1.2.3