diff options
| author | soubiran | 2009-11-13 10:39:10 +0000 |
|---|---|---|
| committer | soubiran | 2009-11-13 10:39:10 +0000 |
| commit | 4f4c8cdf837763ab8ebc5988f37b8b63f8a284e3 (patch) | |
| tree | d01de5626e6cb32b45dda2fd45fd135e368d94c7 /dev | |
| parent | c242a71f206dfbafff457a1229b6322172d64f55 (diff) | |
the inlining computation at functor application was raising not_found when the applied module did not
fulfill the signature of the functor argument. Now Coq gives an understandable error message.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12515 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions