test-suite/success/export_hint.v


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22

Create HintDb foo.

Module Foo.

Axiom F : False.

#[export]
Hint Immediate F : foo.

End Foo.

Goal False.
Proof.
Fail solve [auto with foo].
Abort.

Import Foo.

Goal False.
Proof.
auto with foo.
Qed.