meilleure presentation des commentaires du traducteur

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5168 85f007b7-540e-0410-9357-904b9bb8a0f7

5 files changed, 35 insertions, 11 deletions

diff --git a/interp/modintern.ml b/interp/modintern.ml
index 8a0c8e545..a8c0b22f3 100644
--- a/interp/modintern.ml
+++ b/interp/modintern.ml
@@ -79,9 +79,9 @@ let lookup_modtype (loc,qid) =
 	Modops.error_not_a_modtype_loc loc (string_of_qualid qid)
 
 let transl_with_decl env = function 
-  | CWith_Module (id,qid) ->
+  | CWith_Module ((_,id),qid) ->
       With_Module (id,lookup_module qid)
-  | CWith_Definition (id,c) ->
+  | CWith_Definition ((_,id),c) ->
       With_Definition (id,interp_constr Evd.empty env c)
 
 let rec interp_modtype env = function 
diff --git a/interp/reserve.ml b/interp/reserve.ml
index 8b759b6aa..ed4cdba39 100644
--- a/interp/reserve.ml
+++ b/interp/reserve.ml
@@ -1,6 +1,17 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
+
+(*i $Id$ i*)
+
 (* Reserved names *)
 
 open Util
+open Pp
 open Names
 open Nameops
 open Summary
@@ -24,13 +35,15 @@ let _ =
       Summary.survive_module = false;
       Summary.survive_section = false }
 
-let declare_reserved_type id t = 
+let declare_reserved_type (loc,id) t = 
   if id <> root_of_id id then
-    error ((string_of_id id)^
-    " is not reservable: it must have no trailing digits, quote, or _");
+    user_err_loc(loc,"declare_reserved_type",
+    (pr_id id ++ str
+      " is not reservable: it must have no trailing digits, quote, or _"));
   begin try
     let _ = Idmap.find id !reserve_table in 
-    error ((string_of_id id)^" is already bound to a type")
+    user_err_loc(loc,"declare_reserved_type",
+    (pr_id id++str" is already bound to a type"))
   with Not_found -> () end;
   add_anonymous_leaf (in_reserved (id,t))
 
diff --git a/interp/reserve.mli b/interp/reserve.mli
index 0c60caf9b..2f55e2e6b 100644
--- a/interp/reserve.mli
+++ b/interp/reserve.mli
@@ -1,6 +1,17 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
+
+(*i $Id$ i*)
+
+open Util
 open Names
 open Rawterm
 
-val declare_reserved_type : identifier -> rawconstr -> unit
+val declare_reserved_type : identifier located -> rawconstr -> unit
 val find_reserved_type : identifier -> rawconstr
 val anonymize_if_reserved : name -> rawconstr -> rawconstr
diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index 3e4d3684d..1e8a10a87 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -538,8 +538,8 @@ let rec replace_vars_constr_expr l = function
 (* Concrete syntax for modules and modules types *)
 
 type with_declaration_ast = 
-  | CWith_Module of identifier * qualid located
-  | CWith_Definition of identifier * constr_expr
+  | CWith_Module of identifier located * qualid located
+  | CWith_Definition of identifier located * constr_expr
 
 type module_type_ast = 
   | CMTEident of qualid located
diff --git a/interp/topconstr.mli b/interp/topconstr.mli
index 241d84687..65beaa511 100644
--- a/interp/topconstr.mli
+++ b/interp/topconstr.mli
@@ -149,8 +149,8 @@ val local_binders_length : local_binder list -> int
 (* Concrete syntax for modules and modules types *)
 
 type with_declaration_ast = 
-  | CWith_Module of identifier * qualid located
-  | CWith_Definition of identifier * constr_expr
+  | CWith_Module of identifier located * qualid located
+  | CWith_Definition of identifier located * constr_expr
 
 type module_type_ast = 
   | CMTEident of qualid located