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 +------
 1 file changed, 1 insertion(+), 6 deletions(-)

(limited to 'test-suite')

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