1 files changed, 14 insertions, 0 deletions
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 =