diff options
| author |  coq <coq@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-12-04 16:21:06 +0000 |
|---|---|---|
| committer | coq <coq@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-12-04 16:21:06 +0000 |
| commit | cc92b9228f3463ce06ad457a47ef2a9b1f39a727 (patch) | |
| tree | 4612d294b6ea463adef8baa1fe2a9fc922f12320 | |
| parent | 088bf85a1eb199e3a922d8f5a1ef58573f46d257 (diff) | |
Correction d'un message d'erreur de l'application de non-foncteur
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3375 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | library/declaremods.ml | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/library/declaremods.ml b/library/declaremods.ml index 6cae78bba..7b6c7ec1b 100644 --- a/library/declaremods.ml +++ b/library/declaremods.ml @@ -79,7 +79,7 @@ let modtab_objects = (*let modtab_keep = ref (MPmap.empty : (object_prefix * lib_objects) MPmap.t)*) -(* currently begun interactive module (if any) - its arguments (if it +(* currently started interactive module (if any) - its arguments (if it is a functor) and declared output type *) let openmod_info = ref (([],None) : mod_bound_id list * module_type_entry option) @@ -628,7 +628,9 @@ let rec get_module_substobjs = function (match mbids with | mbid::mbids -> (add_mbid mbid mp subst, mbids, msid, objs) - | [] -> anomaly "Too few arguments in functor") + | [] -> match mexpr with + | MEident _ | MEstruct _ -> error "Application of a non-functor" + | _ -> error "Application of a functor with too few arguments") | MEapply (_,mexpr) -> Modops.error_application_to_not_path mexpr |