diff options
| author | Pierre-Marie Pédrot | 2014-09-09 22:13:08 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2014-09-10 00:16:20 +0200 |
| commit | edfa5e986a25eb7a0719d20b43a618cb5bd4cd95 (patch) | |
| tree | e7af11e344a99b2496d22d2bc100f493bd701b96 /toplevel | |
| parent | 0dd3f0d34873dcd126be8ec48724a310214f38ac (diff) | |
VernacExtend does not dispatch on type anymore.
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/vernacinterp.ml | 8 | ||||
| -rw-r--r-- | toplevel/vernacinterp.mli | 6 |
2 files changed, 7 insertions, 7 deletions
diff --git a/toplevel/vernacinterp.ml b/toplevel/vernacinterp.ml index 2753a3367a..31d1c641cd 100644 --- a/toplevel/vernacinterp.ml +++ b/toplevel/vernacinterp.ml @@ -12,14 +12,14 @@ open Errors (* Table of vernac entries *) let vernac_tab = (Hashtbl.create 51 : - (string, Genarg.raw_generic_argument list -> unit -> unit) Hashtbl.t) + (Vernacexpr.extend_name, (Genarg.raw_generic_argument list -> unit -> unit)) Hashtbl.t) let vinterp_add s f = try Hashtbl.add vernac_tab s f with Failure _ -> errorlabstrm "vinterp_add" - (str"Cannot add the vernac command " ++ str s ++ str" twice.") + (str"Cannot add the vernac command " ++ str (fst s) ++ str" twice.") let overwriting_vinterp_add s f = begin @@ -32,9 +32,9 @@ let overwriting_vinterp_add s f = let vinterp_map s = try Hashtbl.find vernac_tab s - with Not_found -> + with Failure _ | Not_found -> errorlabstrm "Vernac Interpreter" - (str"Cannot find vernac command " ++ str s ++ str".") + (str"Cannot find vernac command " ++ str (fst s) ++ str".") let vinterp_init () = Hashtbl.clear vernac_tab diff --git a/toplevel/vernacinterp.mli b/toplevel/vernacinterp.mli index 3cbbbf05ee..33920ec705 100644 --- a/toplevel/vernacinterp.mli +++ b/toplevel/vernacinterp.mli @@ -8,9 +8,9 @@ (** Interpretation of extended vernac phrases. *) -val vinterp_add : string -> (Genarg.raw_generic_argument list -> unit -> unit) -> unit +val vinterp_add : Vernacexpr.extend_name -> (Genarg.raw_generic_argument list -> unit -> unit) -> unit val overwriting_vinterp_add : - string -> (Genarg.raw_generic_argument list -> unit -> unit) -> unit + Vernacexpr.extend_name -> (Genarg.raw_generic_argument list -> unit -> unit) -> unit val vinterp_init : unit -> unit -val call : ?locality:bool -> string * Genarg.raw_generic_argument list -> unit +val call : ?locality:bool -> Vernacexpr.extend_name * Genarg.raw_generic_argument list -> unit |