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 ++++++++++++++++++++++++++++++++++
 1 file changed, 34 insertions(+)
 create mode 100644 test-suite/ltac2/std_tactics.v

(limited to 'test-suite')

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.
-- 
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 +------
 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