diff options
Diffstat (limited to 'tactics/tacenv.ml')
| -rw-r--r-- | tactics/tacenv.ml | 13 |
1 files changed, 8 insertions, 5 deletions
diff --git a/tactics/tacenv.ml b/tactics/tacenv.ml index dc89a71ef..d2d3f3117 100644 --- a/tactics/tacenv.ml +++ b/tactics/tacenv.ml @@ -15,9 +15,10 @@ open Tacexpr (** Tactic notations (TacAlias) *) type alias = KerName.t +type alias_tactic = Id.t list * glob_tactic_expr let alias_map = Summary.ref ~name:"tactic-alias" - (KNmap.empty : glob_tactic_expr KNmap.t) + (KNmap.empty : alias_tactic KNmap.t) let register_alias key tac = alias_map := KNmap.add key tac !alias_map @@ -31,7 +32,7 @@ let check_alias key = KNmap.mem key !alias_map (** ML tactic extensions (TacML) *) type ml_tactic = - typed_generic_argument list -> Geninterp.interp_sign -> unit Proofview.tactic + Val.t list -> Geninterp.interp_sign -> unit Proofview.tactic module MLName = struct @@ -49,7 +50,7 @@ let pr_tacname t = let tac_tab = ref MLTacMap.empty -let register_ml_tactic ?(overwrite = false) s (t : ml_tactic) = +let register_ml_tactic ?(overwrite = false) s (t : ml_tactic array) = let () = if MLTacMap.mem s !tac_tab then if overwrite then @@ -60,9 +61,11 @@ let register_ml_tactic ?(overwrite = false) s (t : ml_tactic) = in tac_tab := MLTacMap.add s t !tac_tab -let interp_ml_tactic s = +let interp_ml_tactic { mltac_name = s; mltac_index = i } = try - MLTacMap.find s !tac_tab + let tacs = MLTacMap.find s !tac_tab in + let () = if Array.length tacs <= i then raise Not_found in + tacs.(i) with Not_found -> Errors.errorlabstrm "" (str "The tactic " ++ pr_tacname s ++ str " is not installed.") |