From 9b32244199542142502b0ced52a0290eeb411ddb Mon Sep 17 00:00:00 2001 From: herbelin Date: Thu, 28 Nov 2002 23:03:22 +0000 Subject: Bug exception git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3330 85f007b7-540e-0410-9357-904b9bb8a0f7 --- interp/symbols.ml | 9 +++------ 1 file changed, 3 insertions(+), 6 deletions(-) diff --git a/interp/symbols.ml b/interp/symbols.ml index 0d949fb28..3704decd4 100644 --- a/interp/symbols.ml +++ b/interp/symbols.ml @@ -174,12 +174,9 @@ let check_required_module loc sc d = ^(list_last d))) let lookup_numeral_interpreter loc sc = - try - let (dir,interpreter) = Hashtbl.find numeral_interpreter_tab sc in - check_required_module loc sc dir; - interpreter - with Not_found -> - error ("No interpretation for numerals in scope "^sc) + let (dir,interpreter) = Hashtbl.find numeral_interpreter_tab sc in + check_required_module loc sc dir; + interpreter (* Look if some notation or numeral printer in [scope] can be used in the scope stack [scopes], and if yes, using delimiters or not *) -- cgit v1.2.3