diff options
| author | Pierre-Marie Pédrot | 2020-03-12 15:31:26 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-03-18 11:57:19 +0100 |
| commit | d583f810be066929301864765601ff53497bc335 (patch) | |
| tree | 34ca12836c91fef1af681fec92b6ab45201c6b02 /test-suite | |
| parent | 96ec58df041dc0111df0e681269aed9d0e9b571a (diff) | |
Export the user-facing attribute for hint locality.
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/success/export_hint.v | 22 |
1 files changed, 22 insertions, 0 deletions
diff --git a/test-suite/success/export_hint.v b/test-suite/success/export_hint.v new file mode 100644 index 0000000000..e18f7c1bef --- /dev/null +++ b/test-suite/success/export_hint.v @@ -0,0 +1,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. |