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

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