diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2007-10-09 21:47:36 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2007-10-09 21:47:36 +0000 |
| commit | 29c800d48a84e89f2db8a60c64b3f91b59b54384 (patch) | |
| tree | e7fd2a44358ee8286739d9dbf9fea1406d0124ea /INSTALL | |
| parent | 962f845da900095720f93b97c3977be96027c82b (diff) | |
Extraction now checks that the required libraries are indeed loaded (bug #1144)
If a library is Require'd from inside an "opaque" Module (e.g. a module with
an interface given by a ":"), then the required library is not loaded anymore
after closing this module. We add an error in this situation, asking the user
to manually do a Require before performing the Extraction.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10208 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'INSTALL')
0 files changed, 0 insertions, 0 deletions