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 /kernel | |
| 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 'kernel')
| -rw-r--r-- | kernel/modops.ml | 24 |
1 files changed, 14 insertions, 10 deletions
diff --git a/kernel/modops.ml b/kernel/modops.ml index 7ee48c352b..2cc0f17ea9 100644 --- a/kernel/modops.ml +++ b/kernel/modops.ml @@ -363,17 +363,21 @@ let complete_inline_delta_resolver env mp mbid mtb delta = let kn = replace_mp_in_kn (MPbound mbid) mp kn in let con = constant_of_kn kn in let con' = constant_of_delta delta con in - let constant = lookup_constant con' env in - if (not constant.Declarations.const_opaque) then - let constr = Option.map Declarations.force - constant.Declarations.const_body in - if constr = None then - (make_inline delta r) + try + let constant = lookup_constant con' env in + if (not constant.Declarations.const_opaque) then + let constr = Option.map Declarations.force + constant.Declarations.const_body in + if constr = None then + (make_inline delta r) + else + add_inline_constr_delta_resolver con (Option.get constr) + (make_inline delta r) else - add_inline_constr_delta_resolver con (Option.get constr) - (make_inline delta r) - else - (make_inline delta r) + (make_inline delta r) + with + Not_found -> error_no_such_label_sub (con_label con) + (string_of_mp (con_modpath con)) in make_inline delta constants |