diff options
author | Stephane Glondu <steph@glondu.net> | 2010-07-21 09:46:51 +0200 |
---|---|---|
committer | Stephane Glondu <steph@glondu.net> | 2010-07-21 09:46:51 +0200 |
commit | 5b7eafd0f00a16d78f99a27f5c7d5a0de77dc7e6 (patch) | |
tree | 631ad791a7685edafeb1fb2e8faeedc8379318ae /toplevel/vernacinterp.ml | |
parent | da178a880e3ace820b41d38b191d3785b82991f5 (diff) |
Imported Upstream snapshot 8.3~beta0+13298
Diffstat (limited to 'toplevel/vernacinterp.ml')
-rw-r--r-- | toplevel/vernacinterp.ml | 15 |
1 files changed, 7 insertions, 8 deletions
diff --git a/toplevel/vernacinterp.ml b/toplevel/vernacinterp.ml index 41669c47..0924e519 100644 --- a/toplevel/vernacinterp.ml +++ b/toplevel/vernacinterp.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: vernacinterp.ml 11309 2008-08-06 10:30:35Z herbelin $ *) +(* $Id$ *) open Pp open Util @@ -27,24 +27,24 @@ let vernac_tab = (string, Tacexpr.raw_generic_argument list -> unit -> unit) Hashtbl.t) let vinterp_add s f = - try + try Hashtbl.add vernac_tab s f with Failure _ -> errorlabstrm "vinterp_add" (str"Cannot add the vernac command " ++ str s ++ str" twice.") let overwriting_vinterp_add s f = - begin - try - let _ = Hashtbl.find vernac_tab s in Hashtbl.remove vernac_tab s + begin + try + let _ = Hashtbl.find vernac_tab s in Hashtbl.remove vernac_tab s with Not_found -> () end; Hashtbl.add vernac_tab s f let vinterp_map s = - try + try Hashtbl.find vernac_tab s - with Not_found -> + with Not_found -> errorlabstrm "Vernac Interpreter" (str"Cannot find vernac command " ++ str s ++ str".") @@ -62,7 +62,6 @@ let call (opn,converted_args) = hunk() with | Drop -> raise Drop - | ProtectedLoop -> raise ProtectedLoop | e -> if !Flags.debug then msgnl (str"Vernac Interpreter " ++ str !loc); |