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
---
 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 +-
 5 files changed, 6 insertions(+), 18 deletions(-)

(limited to 'user-contrib')

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