diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-03-05 16:42:42 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-03-05 16:42:42 +0000 |
| commit | 19d89158f4e0e4be5998f2ff9b64e90270977a32 (patch) | |
| tree | 99dd65665fdbfe64be95cb870da5e710ec4d8c8e /kernel/mod_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/mod_typing.ml')
| -rw-r--r-- | kernel/mod_typing.ml | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml index bbcabd72a..335c2a94e 100644 --- a/kernel/mod_typing.ml +++ b/kernel/mod_typing.ml @@ -132,12 +132,12 @@ and check_with_aux_def env sign with_decl mp equiv = mod_type_alg = None}) in SEBstruct(before@((l,new_spec)::after)),cb,cst | Some msb -> - error_a_generative_module_expected l + error_generative_module_expected l end | _ -> anomaly "Modtyping:incorrect use of with" with Not_found -> error_no_such_label l - | Reduction.NotConvertible -> error_with_incorrect l + | Reduction.NotConvertible -> error_incorrect_with_constraint l and check_with_aux_mod env sign with_decl mp equiv = let sig_b = match sign with @@ -175,12 +175,12 @@ and check_with_aux_mod env sign with_decl mp equiv = (check_subtypes env' mtb_mp1 (module_type_of_module env' None old)) old.mod_constraints - with Failure _ -> error_with_incorrect (label_of_id id) + with Failure _ -> error_incorrect_with_constraint (label_of_id id) end | Some (SEBident(mp')) -> check_modpath_equiv env' mp1 mp'; old.mod_constraints - | _ -> error_a_generative_module_expected l + | _ -> error_generative_module_expected l in let new_mb = strengthen_and_subst_mb mb_mp1 (MPdot(mp,l)) env false in @@ -220,12 +220,12 @@ and check_with_aux_mod env sign with_decl mp equiv = SEBstruct(before@(l,spec)::after) ,equiv,empty_constraint | _ -> - error_a_generative_module_expected l + error_generative_module_expected l end | _ -> anomaly "Modtyping:incorrect use of with" with Not_found -> error_no_such_label l - | Reduction.NotConvertible -> error_with_incorrect l + | Reduction.NotConvertible -> error_incorrect_with_constraint l and translate_module env mp inl me = match me.mod_entry_expr, me.mod_entry_type with |