diff options
Diffstat (limited to 'tactics/tacenv.mli')
| -rw-r--r-- | tactics/tacenv.mli | 13 |
1 files changed, 8 insertions, 5 deletions
diff --git a/tactics/tacenv.mli b/tactics/tacenv.mli index 87cdce652..88b54993b 100644 --- a/tactics/tacenv.mli +++ b/tactics/tacenv.mli @@ -17,10 +17,13 @@ open Tacexpr type alias = KerName.t (** Type of tactic alias, used in the [TacAlias] node. *) -val register_alias : alias -> glob_tactic_expr -> unit +type alias_tactic = Id.t list * glob_tactic_expr +(** Contents of a tactic notation *) + +val register_alias : alias -> alias_tactic -> unit (** Register a tactic alias. *) -val interp_alias : alias -> glob_tactic_expr +val interp_alias : alias -> alias_tactic (** Recover the the body of an alias. Raises an anomaly if it does not exist. *) val check_alias : alias -> bool @@ -61,11 +64,11 @@ val ltac_entries : unit -> ltac_entry KNmap.t (** {5 ML tactic extensions} *) type ml_tactic = - typed_generic_argument list -> Geninterp.interp_sign -> unit Proofview.tactic + Val.t list -> Geninterp.interp_sign -> unit Proofview.tactic (** Type of external tactics, used by [TacML]. *) -val register_ml_tactic : ?overwrite:bool -> ml_tactic_name -> ml_tactic -> unit +val register_ml_tactic : ?overwrite:bool -> ml_tactic_name -> ml_tactic array -> unit (** Register an external tactic. *) -val interp_ml_tactic : ml_tactic_name -> ml_tactic +val interp_ml_tactic : ml_tactic_entry -> ml_tactic (** Get the named tactic. Raises a user error if it does not exist. *) |