diff options
| author |  barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-03-20 19:15:47 +0000 |
|---|---|---|
| committer | barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-03-20 19:15:47 +0000 |
| commit | a0d3c8c3268f23c3fed89f9c30df9c3bbd604034 (patch) | |
| tree | 9ee5c45e53a1d38571825a7cfcae33d4f18ba23f /library/library.mllib | |
| parent | eb04887fe4d48deabc029e067a8d0e4515879e8a (diff) | |
replaced dir_load by load_file because dir_load does not raise an exception when loading fails
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12000 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'library/library.mllib')
0 files changed, 0 insertions, 0 deletions