diff options
| author | herbelin | 2011-03-05 16:42:42 +0000 |
|---|---|---|
| committer | herbelin | 2011-03-05 16:42:42 +0000 |
| commit | 19d89158f4e0e4be5998f2ff9b64e90270977a32 (patch) | |
| tree | 99dd65665fdbfe64be95cb870da5e710ec4d8c8e /kernel/safe_typing.ml | |
| parent | 0c2dd4a32538ebda7c964c249f158054b6cc2e1a (diff) | |
Moving printing of module typing errors upwards to himsg.ml so as to
be able to call term printers.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13886 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/safe_typing.ml')
| -rw-r--r-- | kernel/safe_typing.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index 66c731a9de..8f4ec76f84 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -367,7 +367,7 @@ let end_module l restype senv = | STRUCT params -> params, (List.length params > 0) in if l <> modinfo.label then error_incompatible_labels l modinfo.label; - if not (empty_context senv.env) then error_local_context None; + if not (empty_context senv.env) then error_non_empty_local_context None; let functorize_struct tb = List.fold_left (fun mtb (arg_id,arg_b) -> @@ -574,7 +574,7 @@ let end_modtype l senv = | SIG params -> params in if l <> modinfo.label then error_incompatible_labels l modinfo.label; - if not (empty_context senv.env) then error_local_context None; + if not (empty_context senv.env) then error_non_empty_local_context None; let auto_tb = SEBstruct (List.rev senv.revstruct) in |