diff options
| author | Emilio Jesus Gallego Arias | 2017-01-26 11:38:19 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2017-01-26 12:57:05 +0100 |
| commit | 86116b181bb866c7f63a37796e1388f731ce7204 (patch) | |
| tree | 2e15c5292461a2719309e49bf25e0b0900175985 /dev/base_include | |
| parent | a6f687852c0c7509a06fdf16c0af29129b3566d5 (diff) | |
[native comp] Improve error message on linking error.
The native compiler doesn't support `Require` inside `Module` sections
in some cases, we improve the error message. See:
https://coq.inria.fr/bugs/show_bug.cgi?id=4335
This patch improves the error message and gives the user some
feedback.
Diffstat (limited to 'dev/base_include')
0 files changed, 0 insertions, 0 deletions