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