unify for Ltac2

Fixes #14083

1 files changed, 34 insertions, 0 deletions

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.