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

10 files changed, 316 insertions, 140 deletions

diff --git a/interp/modintern.ml b/interp/modintern.ml
index 5866073ccd..c127590923 100644
--- a/interp/modintern.ml
+++ b/interp/modintern.ml
@@ -14,6 +14,54 @@ open Libnames
 open Topconstr
 open Constrintern
 
+type module_internalization_error =
+  | NotAModuleNorModtype of string
+  | IncorrectWithInModule
+  | IncorrectModuleApplication
+
+exception ModuleInternalizationError of module_internalization_error
+
+(*
+val error_declaration_not_path : module_struct_entry -> 'a
+
+val error_not_a_functor :  module_struct_entry -> 'a
+
+val error_not_equal : module_path -> module_path -> 'a
+
+val error_result_must_be_signature : unit -> 'a
+
+oval error_not_a_modtype_loc : loc -> string -> 'a
+
+val error_not_a_module_loc : loc -> string -> 'a
+
+val error_not_a_module_or_modtype_loc : loc -> string -> 'a
+
+val error_with_in_module : unit -> 'a
+
+val error_application_to_module_type : unit -> 'a
+*)
+
+let error_result_must_be_signature () =
+  error "The result module type must be a signature."
+
+let error_not_a_modtype_loc loc s =
+  Compat.Loc.raise loc (Modops.ModuleTypingError (Modops.NotAModuleType s))
+
+let error_not_a_module_loc loc s =
+  Compat.Loc.raise loc (Modops.ModuleTypingError (Modops.NotAModule s))
+
+let error_not_a_module_nor_modtype_loc loc s =
+  Compat.Loc.raise loc (ModuleInternalizationError (NotAModuleNorModtype s))
+
+let error_incorrect_with_in_module () =
+  raise (ModuleInternalizationError IncorrectWithInModule)
+
+let error_application_to_module_type () =
+  raise (ModuleInternalizationError IncorrectModuleApplication)
+
+
+
+
 let rec make_mp mp = function
     [] -> mp
   | h::tl -> make_mp (MPdot(mp, label_of_id h)) tl
@@ -68,7 +116,7 @@ let lookup_module (loc,qid) =
     let mp = Nametab.locate_module qid in
       Dumpglob.dump_modref loc mp "modtype"; mp
   with
-    | Not_found -> Modops.error_not_a_module_loc loc (string_of_qualid qid)
+    | Not_found -> error_not_a_module_loc loc (string_of_qualid qid)
 
 let lookup_modtype (loc,qid) =
   try
@@ -76,7 +124,7 @@ let lookup_modtype (loc,qid) =
       Dumpglob.dump_modref loc mp "mod"; mp
   with
     | Not_found ->
-	Modops.error_not_a_modtype_loc loc (string_of_qualid qid)
+	error_not_a_modtype_loc loc (string_of_qualid qid)
 
 let lookup_module_or_modtype (loc,qid) =
   try
@@ -86,7 +134,7 @@ let lookup_module_or_modtype (loc,qid) =
     let mp = Nametab.locate_modtype qid in
     Dumpglob.dump_modref loc mp "mod"; (mp,false)
   with Not_found ->
-    Modops.error_not_a_module_or_modtype_loc loc (string_of_qualid qid)
+    error_not_a_module_nor_modtype_loc loc (string_of_qualid qid)
 
 let transl_with_decl env = function
   | CWith_Module ((_,fqid),qid) ->
@@ -101,7 +149,7 @@ let rec interp_modexpr env = function
       let me1 = interp_modexpr env me1 in
       let me2 = interp_modexpr env me2 in
 	MSEapply(me1,me2)
-  | CMwith _ -> Modops.error_with_in_module ()
+  | CMwith _ -> error_incorrect_with_in_module ()
 
 
 let rec interp_modtype env = function
@@ -123,10 +171,10 @@ let rec interp_modexpr_or_modtype env = function
   | CMapply (me1,me2) ->
       let me1,ismod1 = interp_modexpr_or_modtype env me1 in
       let me2,ismod2 = interp_modexpr_or_modtype env me2 in
-      if not ismod2 then Modops.error_application_to_module_type ();
+      if not ismod2 then error_application_to_module_type ();
       (MSEapply (me1,me2), ismod1)
   | CMwith (me,decl) ->
       let me,ismod = interp_modexpr_or_modtype env me in
       let decl = transl_with_decl env decl in
-      if ismod then Modops.error_with_in_module ();
+      if ismod then error_incorrect_with_in_module ();
       (MSEwith(me,decl), ismod)
diff --git a/interp/modintern.mli b/interp/modintern.mli
index a294806635..71a00c2fef 100644
--- a/interp/modintern.mli
+++ b/interp/modintern.mli
@@ -14,8 +14,17 @@ open Libnames
 open Names
 open Topconstr
 
+(** Module internalization errors *)
+
+type module_internalization_error =
+  | NotAModuleNorModtype of string
+  | IncorrectWithInModule
+  | IncorrectModuleApplication
+
+exception ModuleInternalizationError of module_internalization_error
+
 (** Module expressions and module types are interpreted relatively to
-   eventual functor or funsig arguments. *)
+   possible functor or functor signature arguments. *)
 
 val interp_modtype : env -> module_ast -> module_struct_entry
 
diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml
index bbcabd72a2..335c2a94ee 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
diff --git a/kernel/modops.ml b/kernel/modops.ml
index 302d251949..6d4ebb989b 100644
--- a/kernel/modops.ml
+++ b/kernel/modops.ml
@@ -25,19 +25,6 @@ open Environ
 open Entries
 open Mod_subst
 
-let error_existing_label l = 
-  error ("The label "^string_of_label l^" is already declared.")
-
-let error_declaration_not_path _ = error "Declaration is not a path."
-
-let error_application_to_not_path _ = error "Application to not path."
-
-let error_not_a_functor _ = error "Application of not a functor."
-
-let error_incompatible_modtypes _ _ = error "Incompatible module types."
-
-let error_not_equal _ _ = error "Non equal modules."
-
 type signature_mismatch_error =
   | InductiveFieldExpected of mutual_inductive_body
   | DefinitionFieldExpected
@@ -57,104 +44,83 @@ type signature_mismatch_error =
   | NotEqualInductiveAliases
   | NoTypeConstraintExpected
 
-let explain_not_match_error = function
-  | InductiveFieldExpected _ ->
-    strbrk "an inductive definition is expected"
-  | DefinitionFieldExpected ->
-    strbrk "a definition is expected"
-  | ModuleFieldExpected ->
-    strbrk "a module is expected"
-  | ModuleTypeFieldExpected ->
-    strbrk "a module type is expected"
-  | NotConvertibleInductiveField id | NotConvertibleConstructorField id ->
-    str "types given to " ++ str (string_of_id id) ++ str " differ"
-  | NotConvertibleBodyField ->
-    str "the body of definitions differs"
-  | NotConvertibleTypeField ->
-    str "types differ"
-  | NotSameConstructorNamesField ->
-    str "constructor names differ"
-  | NotSameInductiveNameInBlockField ->
-    str "inductive types names differ"
-  | FiniteInductiveFieldExpected isfinite ->
-    str "type is expected to be " ++
-    str (if isfinite then "coinductive" else "inductive")
-  | InductiveNumbersFieldExpected n ->
-    str "number of inductive types differs"
-  | InductiveParamsNumberField n ->
-    str "inductive type has not the right number of parameters"
-  | RecordFieldExpected isrecord ->
-    str "type is expected " ++ str (if isrecord then "" else "not ") ++
-    str "to be a record"
-  | RecordProjectionsExpected nal ->
-    (if List.length nal >= 2 then str "expected projection names are "
-     else str "expected projection name is ") ++
-    pr_enum (function Name id -> str (string_of_id id) | _ -> str "_") nal
-  | NotEqualInductiveAliases ->
-    str "Aliases to inductive types do not match"
-  | NoTypeConstraintExpected ->
-    strbrk "a definition whose type is constrained can only be subtype of a definition whose type is itself constrained"
-
-let error_not_match l _ why =
-  errorlabstrm ""
-    (str "Signature components for label " ++ str (string_of_label l) ++
-     str " do not match:" ++ spc () ++ explain_not_match_error why ++ str ".")
-
-let error_no_such_label l = error ("No such label "^string_of_label l^".")
-
-let error_incompatible_labels l l' = 
-  error ("Opening and closing labels are not the same: "
-	 ^string_of_label l^" <> "^string_of_label l'^" !")
-
-let error_result_must_be_signature () = 
-  error "The result module type must be a signature."
+type module_typing_error =
+  | SignatureMismatch of label * structure_field_body * signature_mismatch_error
+  | LabelAlreadyDeclared of label
+  | ApplicationToNotPath of module_struct_entry
+  | NotAFunctor of struct_expr_body
+  | IncompatibleModuleTypes of module_type_body * module_type_body
+  | NotEqualModulePaths of module_path * module_path
+  | NoSuchLabel of label
+  | IncompatibleLabels of label * label
+  | SignatureExpected of struct_expr_body
+  | NoModuleToEnd
+  | NoModuleTypeToEnd
+  | NotAModule of string
+  | NotAModuleType of string
+  | NotAConstant of label
+  | IncorrectWithConstraint of label
+  | GenerativeModuleExpected of label
+  | NonEmptyLocalContect of label option
+  | LabelMissing of label * string
 
-let error_signature_expected mtb =
-  error "Signature expected."
+exception ModuleTypingError of module_typing_error
 
-let error_no_module_to_end _ = 
-  error "No open module to end."
+let error_existing_label l =
+  raise (ModuleTypingError (LabelAlreadyDeclared l))
 
-let error_no_modtype_to_end _ =
-  error "No open module type to end."
+let error_application_to_not_path mexpr =
+  raise (ModuleTypingError (ApplicationToNotPath mexpr))
 
-let error_not_a_modtype_loc loc s = 
-  user_err_loc (loc,"",str ("\""^s^"\" is not a module type."))
+let error_not_a_functor mtb =
+  raise (ModuleTypingError (NotAFunctor mtb))
 
-let error_not_a_module_loc loc s = 
-  user_err_loc (loc,"",str ("\""^s^"\" is not a module."))
+let error_incompatible_modtypes mexpr1 mexpr2 =
+  raise (ModuleTypingError (IncompatibleModuleTypes (mexpr1,mexpr2)))
 
-let error_not_a_module_or_modtype_loc loc s =
-  user_err_loc (loc,"",str ("\""^s^"\" is not a module or module type."))
+let error_not_equal_modpaths mp1 mp2 =
+  raise (ModuleTypingError (NotEqualModulePaths (mp1,mp2)))
 
-let error_not_a_module s = error_not_a_module_loc dummy_loc s
+let error_signature_mismatch l spec why =
+  raise (ModuleTypingError (SignatureMismatch (l,spec,why)))
 
-let error_not_a_constant l = 
-  error ("\""^(string_of_label l)^"\" is not a constant.")
+let error_no_such_label l =
+  raise (ModuleTypingError (NoSuchLabel l))
 
-let error_with_incorrect l =
-  error ("Incorrect constraint for label \""^(string_of_label l)^"\".")
+let error_incompatible_labels l l' =
+  raise (ModuleTypingError (IncompatibleLabels (l,l')))
 
-let error_a_generative_module_expected l =
-  error ("The module " ^ string_of_label l ^ " is not generative. Only " ^
-         "components of generative modules can be changed using the \"with\" " ^
-         "construct.")
+let error_signature_expected mtb =
+  raise (ModuleTypingError (SignatureExpected mtb))
 
-let error_local_context lo = 
-  match lo with
-      None -> 
-	error ("The local context is not empty.")
-    | (Some l) ->
-	error ("The local context of the component "^
-	       (string_of_label l)^" is not empty.")
+let error_no_module_to_end _ =
+  raise (ModuleTypingError NoModuleToEnd)
 
+let error_no_modtype_to_end _ =
+  raise (ModuleTypingError NoModuleTypeToEnd)
 
-let error_no_such_label_sub l l1 =
-  error ("The field "^(string_of_label l)^" is missing in "^l1^".")
+let error_not_a_modtype s =
+  raise (ModuleTypingError (NotAModuleType s))
+
+let error_not_a_module s =
+  raise (ModuleTypingError (NotAModule s))
+
+let error_not_a_constant l =
+  raise (ModuleTypingError (NotAConstant l))
 
-let error_with_in_module _ = error "The syntax \"with\" is not allowed for modules."
+let error_incorrect_with_constraint l =
+  raise (ModuleTypingError (IncorrectWithConstraint l))
+
+let error_generative_module_expected l =
+  raise (ModuleTypingError (GenerativeModuleExpected l))
+
+let error_non_empty_local_context lo =
+  raise (ModuleTypingError (NonEmptyLocalContect lo))
+
+let error_no_such_label_sub l l1 =
+  raise (ModuleTypingError (LabelMissing (l,l1)))
 
-let error_application_to_module_type _ = error "Module application to a module type."
+(************************)
 
 let destr_functor env mtb =
   match mtb with
@@ -181,7 +147,7 @@ let check_modpath_equiv env mp1 mp2 =
     let mb2=lookup_module mp2 env in
       if (delta_of_mp mb1.mod_delta mp1)=(delta_of_mp mb2.mod_delta mp2)
       then ()
-      else error_not_equal mp1 mp2
+      else error_not_equal_modpaths mp1 mp2
 	
 let rec subst_with_body sub = function
   | With_module_body(id,mp) ->
diff --git a/kernel/modops.mli b/kernel/modops.mli
index cf8d62043f..35be04665b 100644
--- a/kernel/modops.mli
+++ b/kernel/modops.mli
@@ -72,53 +72,56 @@ type signature_mismatch_error =
   | NotEqualInductiveAliases
   | NoTypeConstraintExpected
 
-val error_existing_label : label -> 'a
+type module_typing_error =
+  | SignatureMismatch of label * structure_field_body * signature_mismatch_error
+  | LabelAlreadyDeclared of label
+  | ApplicationToNotPath of module_struct_entry
+  | NotAFunctor of struct_expr_body
+  | IncompatibleModuleTypes of module_type_body * module_type_body
+  | NotEqualModulePaths of module_path * module_path
+  | NoSuchLabel of label
+  | IncompatibleLabels of label * label
+  | SignatureExpected of struct_expr_body
+  | NoModuleToEnd
+  | NoModuleTypeToEnd
+  | NotAModule of string
+  | NotAModuleType of string
+  | NotAConstant of label
+  | IncorrectWithConstraint of label
+  | GenerativeModuleExpected of label
+  | NonEmptyLocalContect of label option
+  | LabelMissing of label * string
+
+exception ModuleTypingError of module_typing_error
 
-val error_declaration_not_path : module_struct_entry -> 'a
+val error_existing_label : label -> 'a
 
 val error_application_to_not_path : module_struct_entry -> 'a
 
-val error_not_a_functor :  module_struct_entry -> 'a
-
 val error_incompatible_modtypes :
   module_type_body -> module_type_body -> 'a
 
-val error_not_equal : module_path -> module_path -> 'a
-
-val error_not_match :
+val error_signature_mismatch :
   label -> structure_field_body -> signature_mismatch_error -> 'a
 
 val error_incompatible_labels : label -> label -> 'a
 
 val error_no_such_label : label -> 'a
 
-val error_result_must_be_signature : unit -> 'a
-
 val error_signature_expected : struct_expr_body -> 'a
 
 val error_no_module_to_end : unit -> 'a
 
 val error_no_modtype_to_end : unit -> 'a
 
-val error_not_a_modtype_loc : loc -> string -> 'a
-
-val error_not_a_module_loc : loc -> string -> 'a
-
-val error_not_a_module_or_modtype_loc : loc -> string -> 'a
-
 val error_not_a_module : string -> 'a
 
 val error_not_a_constant : label -> 'a
 
-val error_with_incorrect : label -> 'a
+val error_incorrect_with_constraint : label -> 'a
 
-val error_a_generative_module_expected : label -> 'a
+val error_generative_module_expected : label -> 'a
 
-val error_local_context : label option -> 'a
+val error_non_empty_local_context : label option -> 'a
 
 val error_no_such_label_sub : label->string->'a
-
-val error_with_in_module : unit -> 'a
-
-val error_application_to_module_type : unit -> 'a
-
diff --git a/kernel/names.ml b/kernel/names.ml
index 6e39b35bb3..4466f558f9 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -107,6 +107,7 @@ let label_of_mbid (_,s,_) = s
 
 let mk_label l = l
 let string_of_label = string_of_id
+let pr_label l = str (string_of_label l)
 
 let id_of_label l = l
 let label_of_id id = id
diff --git a/kernel/names.mli b/kernel/names.mli
index 2d112b32ac..acc764028f 100644
--- a/kernel/names.mli
+++ b/kernel/names.mli
@@ -47,6 +47,7 @@ type label
 
 val mk_label : string -> label
 val string_of_label : label -> string
+val pr_label : label -> Pp.std_ppcmds
 
 val label_of_id : identifier -> label
 val id_of_label : label -> identifier
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
diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml
index 8085575217..0c72995080 100644
--- a/kernel/subtyping.ml
+++ b/kernel/subtyping.ml
@@ -78,7 +78,7 @@ let check_conv_error error why cst f env a1 a2 =
 let check_inductive cst env mp1 l info1 mp2 mib2 spec2 subst1 subst2 reso1 reso2= 
   let kn1 = make_mind mp1 empty_dirpath l in
   let kn2 = make_mind mp2 empty_dirpath l in
-  let error why = error_not_match l spec2 why in
+  let error why = error_signature_mismatch l spec2 why in
   let check_conv why cst f = check_conv_error error why cst f in
   let mib1 =
     match info1 with
@@ -201,7 +201,7 @@ let check_inductive cst env mp1 l info1 mp2 mib2 spec2 subst1 subst2 reso1 reso2
 
     
 let check_constant cst env mp1 l info1 cb2 spec2 subst1 subst2 = 
-  let error why = error_not_match l spec2 why in
+  let error why = error_signature_mismatch l spec2 why in
   let check_conv cst f = check_conv_error error cst f in
   let check_type cst env t1 t2 =
 
@@ -353,13 +353,13 @@ and check_signatures cst env mp1 sig1 mp2 sig2 subst1 subst2 reso1 reso2=
 	      match info1 with
 		| Module msb -> check_modules cst env msb msb2 
 		    subst1 subst2
-		| _ -> error_not_match l spec2 ModuleFieldExpected
+		| _ -> error_signature_mismatch l spec2 ModuleFieldExpected
 	    end
 	| SFBmodtype mtb2 ->
 	    let mtb1 =
 	      match info1 with
 		| Modtype mtb -> mtb
-		| _ -> error_not_match l spec2 ModuleTypeFieldExpected
+		| _ -> error_signature_mismatch l spec2 ModuleTypeFieldExpected
 	    in
 	    let env = add_module (module_body_of_type mtb2.typ_mp mtb2)
 	      (add_module (module_body_of_type mtb1.typ_mp mtb1) env) in
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index 9443217f1b..6af1f9d56c 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -155,7 +155,7 @@ let explain_generalization env (name,var) j =
 
 let explain_actual_type env sigma j pt =
   let j = j_nf_betaiotaevar sigma j in
-  let pt = nf_betaiota sigma pt in
+  let pt = Reductionops.nf_betaiota sigma pt in
   let pe = pr_ne_context_of (str "In environment") env in
   let (pc,pct) = pr_ljudge_env env j in
   let pt = pr_lconstr_env env pt in
@@ -528,6 +528,154 @@ let explain_pretype_error env sigma err =
   | NonLinearUnification (m,c) -> explain_non_linear_unification env m c
   | TypingError t -> explain_type_error env sigma t
 
+(* Module errors *)
+
+open Modops
+
+let explain_not_match_error = function
+  | InductiveFieldExpected _ ->
+    strbrk "an inductive definition is expected"
+  | DefinitionFieldExpected ->
+    strbrk "a definition is expected"
+  | ModuleFieldExpected ->
+    strbrk "a module is expected"
+  | ModuleTypeFieldExpected ->
+    strbrk "a module type is expected"
+  | NotConvertibleInductiveField id | NotConvertibleConstructorField id ->
+    str "types given to " ++ str (string_of_id id) ++ str " differ"
+  | NotConvertibleBodyField ->
+    str "the body of definitions differs"
+  | NotConvertibleTypeField ->
+    str "types differ"
+  | NotSameConstructorNamesField ->
+    str "constructor names differ"
+  | NotSameInductiveNameInBlockField ->
+    str "inductive types names differ"
+  | FiniteInductiveFieldExpected isfinite ->
+    str "type is expected to be " ++
+    str (if isfinite then "coinductive" else "inductive")
+  | InductiveNumbersFieldExpected n ->
+    str "number of inductive types differs"
+  | InductiveParamsNumberField n ->
+    str "inductive type has not the right number of parameters"
+  | RecordFieldExpected isrecord ->
+    str "type is expected " ++ str (if isrecord then "" else "not ") ++
+    str "to be a record"
+  | RecordProjectionsExpected nal ->
+    (if List.length nal >= 2 then str "expected projection names are "
+     else str "expected projection name is ") ++
+    pr_enum (function Name id -> str (string_of_id id) | _ -> str "_") nal
+  | NotEqualInductiveAliases ->
+    str "Aliases to inductive types do not match"
+  | NoTypeConstraintExpected ->
+    strbrk "a definition whose type is constrained can only be subtype of a definition whose type is itself constrained"
+
+let explain_signature_mismatch l spec why =
+  str "Signature components for label " ++ str (string_of_label l) ++
+  str " do not match:" ++ spc () ++ explain_not_match_error why ++ str "."
+
+let explain_label_already_declared l =
+  str ("The label "^string_of_label l^" is already declared.")
+
+let explain_application_to_not_path _ =
+  str "Application to not path."
+
+let explain_not_a_functor mtb =
+  str "Application of not a functor."
+
+let explain_incompatible_module_types mexpr1 mexpr2 =
+  str "Incompatible module types."
+
+let explain_not_equal_module_paths mp1 mp2 =
+  str "Non equal modules."
+
+let explain_no_such_label l =
+  str "No such label " ++ str (string_of_label l) ++ str "."
+
+let explain_incompatible_labels l l' =
+  str "Opening and closing labels are not the same: " ++
+  str (string_of_label l) ++ str " <> " ++ str (string_of_label l') ++ str "!"
+
+let explain_signature_expected mtb =
+  str "Signature expected."
+
+let explain_no_module_to_end () =
+  str "No open module to end."
+
+let explain_no_module_type_to_end () =
+  str "No open module type to end."
+
+let explain_not_a_module s =
+  quote (str s) ++ str " is not a module."
+
+let explain_not_a_module_type s =
+  quote (str s) ++ str " is not a module type."
+
+let explain_not_a_constant l =
+  quote (pr_label l) ++ str " is not a constant."
+
+let explain_incorrect_label_constraint l =
+  str "Incorrect constraint for label " ++
+  quote (pr_label l) ++ str "."
+
+let explain_generative_module_expected l =
+  str "The module " ++ str (string_of_label l) ++
+  strbrk " is not generative. Only components of generative modules can be changed using the \"with\" construct."
+
+let explain_non_empty_local_context = function
+  | None -> str "The local context is not empty."
+  | Some l ->
+      str "The local context of the component " ++
+      str (string_of_label l) ++ str " is not empty."
+
+let explain_label_missing l s =
+  str "The field " ++ str (string_of_label l) ++ str " is missing in "
+  ++ str s ++ str "."
+
+let explain_module_error env sigma = function
+  | SignatureMismatch (l,spec,err) -> explain_signature_mismatch l spec err
+  | LabelAlreadyDeclared l -> explain_label_already_declared l
+  | ApplicationToNotPath mexpr -> explain_application_to_not_path mexpr
+  | NotAFunctor mtb -> explain_not_a_functor mtb
+  | IncompatibleModuleTypes (m1,m2) -> explain_incompatible_module_types m1 m2
+  | NotEqualModulePaths (mp1,mp2) -> explain_not_equal_module_paths mp1 mp2
+  | NoSuchLabel l -> explain_no_such_label l
+  | IncompatibleLabels (l1,l2) -> explain_incompatible_labels l1 l2
+  | SignatureExpected mtb -> explain_signature_expected mtb
+  | NoModuleToEnd -> explain_no_module_to_end ()
+  | NoModuleTypeToEnd -> explain_no_module_type_to_end ()
+  | NotAModule s -> explain_not_a_module s
+  | NotAModuleType s -> explain_not_a_module_type s
+  | NotAConstant l -> explain_not_a_constant l
+  | IncorrectWithConstraint l -> explain_incorrect_label_constraint l
+  | GenerativeModuleExpected l -> explain_generative_module_expected l
+  | NonEmptyLocalContect lopt -> explain_non_empty_local_context lopt
+  | LabelMissing (l,s) -> explain_label_missing l s
+
+(* Module internalization errors *)
+
+(*
+let explain_declaration_not_path _ =
+  str "Declaration is not a path."
+
+*)
+
+let explain_not_module_nor_modtype s =
+  quote (str s) ++ str " is not a module or module type."
+
+let explain_incorrect_with_in_module () =
+  str "The syntax \"with\" is not allowed for modules."
+
+let explain_incorrect_module_application () =
+  str "Module application to a module type."
+
+open Modintern
+
+let explain_module_internalization_error = function
+  | NotAModuleNorModtype s -> explain_not_module_nor_modtype s
+  | IncorrectWithInModule -> explain_incorrect_with_in_module ()
+  | IncorrectModuleApplication -> explain_incorrect_module_application ()
+
 (* Typeclass errors *)
 
 let explain_not_a_class env c =