diff options
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/vernacentries.ml | 10 |
1 files changed, 8 insertions, 2 deletions
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 0d3f38d139..b125a86636 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -957,9 +957,15 @@ let interp_filter_in m = function let vernac_import export refl = let import_mod (qid,f) = - let m = try Nametab.locate_module qid + let loc = qid.loc in + let m = try + let m = Nametab.locate_module qid in + let () = if Modops.is_functor (Global.lookup_module m).Declarations.mod_type + then CErrors.user_err ?loc Pp.(str "Cannot import functor " ++ pr_qualid qid ++ str".") + in + m with Not_found -> - CErrors.user_err Pp.(str "Cannot find module " ++ pr_qualid qid) + CErrors.user_err ?loc Pp.(str "Cannot find module " ++ pr_qualid qid) in let f = interp_filter_in m f in Declaremods.import_module f ~export m |