diff options
| author | Samuel Gruetter | 2021-04-08 19:41:18 -0400 |
|---|---|---|
| committer | Samuel Gruetter | 2021-04-08 19:41:18 -0400 |
| commit | 807ea5f44ca74c2b2743ed0719e3cbdc46639da7 (patch) | |
| tree | 5739647ab624c4ec2665b956ed75bf71b60f4adf /test-suite | |
| parent | fb63ec7c10076d156caa43f73bad4f69653862a6 (diff) | |
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
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/ltac2/std_tactics.v | 7 |
1 files changed, 1 insertions, 6 deletions
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. |