diff options
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. |