diff options
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); |