diff options
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/symbols.ml | 6 | ||||
| -rw-r--r-- | interp/symbols.mli | 2 |
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 *) |