Localisation erreur interp_notation

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

2 files changed, 5 insertions, 3 deletions

diff --git a/interp/symbols.ml b/interp/symbols.ml
index 32d74b651a..8ca1d207c6 100644
--- a/interp/symbols.ml
+++ b/interp/symbols.ml
@@ -288,14 +288,16 @@ let rec find_interpretation f = function
       with Not_found -> find_interpretation f scopes)
   | [] -> raise Not_found
 
-let rec interp_notation ntn scopes =
+let rec interp_notation loc ntn scopes =
   let f sc =
     let scope = find_scope sc in
     let (pat,df,pp8only) = Stringmap.find ntn scope.notations in
     if pp8only then raise Not_found;
     pat,(df,if sc = default_scope then None else Some sc) in
   try find_interpretation f (List.fold_right push_scope scopes !scope_stack)
-  with Not_found -> error ("Unknown interpretation for notation \""^ntn^"\"")
+  with Not_found -> 
+    user_err_loc
+      (loc,"",str ("Unknown interpretation for notation \""^ntn^"\""))
 
 let uninterp_notations c =
   Gmapl.find (rawconstr_key c) !notations_key_table
diff --git a/interp/symbols.mli b/interp/symbols.mli
index a86ed49f1b..4932b90d5f 100644
--- a/interp/symbols.mli
+++ b/interp/symbols.mli
@@ -93,7 +93,7 @@ val declare_notation_interpretation : notation -> scope_name option ->
 val declare_uninterpretation : interp_rule -> interpretation -> unit
 
 (* Returns the interpretation bound to a notation *)
-val interp_notation : notation -> scope_name list -> 
+val interp_notation : loc -> notation -> scope_name list -> 
       interpretation * ((dir_path * string) * scope_name option)
 
 (* Returns the possible notations for a given term *)