From 19d89158f4e0e4be5998f2ff9b64e90270977a32 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sat, 5 Mar 2011 16:42:42 +0000
Subject: 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
---
 kernel/mod_typing.ml | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

(limited to 'kernel/mod_typing.ml')

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
-- 
cgit v1.2.3