diff options
Diffstat (limited to 'plugins/ltac/tacentries.mli')
| -rw-r--r-- | plugins/ltac/tacentries.mli | 15 |
1 files changed, 9 insertions, 6 deletions
diff --git a/plugins/ltac/tacentries.mli b/plugins/ltac/tacentries.mli index 9bba9ba71..138a584e0 100644 --- a/plugins/ltac/tacentries.mli +++ b/plugins/ltac/tacentries.mli @@ -12,10 +12,12 @@ open Vernacexpr open Tacexpr +open Vernacinterp (** {5 Tactic Definitions} *) -val register_ltac : locality_flag -> Tacexpr.tacdef_body list -> unit +val register_ltac : locality_flag -> ?deprecation:deprecation -> + Tacexpr.tacdef_body list -> unit (** Adds new Ltac definitions to the environment. *) (** {5 Tactic Notations} *) @@ -34,8 +36,8 @@ type argument = Genarg.ArgT.any Extend.user_symbol leaves. *) val add_tactic_notation : - locality_flag -> int -> raw_argument grammar_tactic_prod_item_expr list -> - raw_tactic_expr -> unit + locality_flag -> int -> ?deprecation:deprecation -> raw_argument + grammar_tactic_prod_item_expr list -> raw_tactic_expr -> unit (** [add_tactic_notation local level prods expr] adds a tactic notation in the environment at level [level] with locality [local] made of the grammar productions [prods] and returning the body [expr] *) @@ -47,7 +49,7 @@ val register_tactic_notation_entry : string -> ('a, 'b, 'c) Genarg.genarg_type - to finding an argument by name (as in {!Genarg}) if there is none matching. *) -val add_ml_tactic_notation : ml_tactic_name -> level:int -> +val add_ml_tactic_notation : ml_tactic_name -> level:int -> ?deprecation:deprecation -> argument grammar_tactic_prod_item_expr list list -> unit (** A low-level variant of {!add_tactic_notation} used by the TACTIC EXTEND ML-side macro. *) @@ -55,7 +57,7 @@ val add_ml_tactic_notation : ml_tactic_name -> level:int -> (** {5 Tactic Quotations} *) val create_ltac_quotation : string -> - ('grm Loc.located -> raw_tactic_arg) -> ('grm Pcoq.Gram.entry * int option) -> unit + ('grm Loc.located -> raw_tactic_arg) -> ('grm Pcoq.Entry.t * int option) -> unit (** [create_ltac_quotation name f e] adds a quotation rule to Ltac, that is, Ltac grammar now accepts arguments of the form ["name" ":" "(" <e> ")"], and generates an argument using [f] on the entry parsed by [e]. *) @@ -78,4 +80,5 @@ type _ ty_sig = type ty_ml = TyML : 'r ty_sig * 'r -> ty_ml -val tactic_extend : string -> string -> level:Int.t -> ty_ml list -> unit +val tactic_extend : string -> string -> level:Int.t -> + ?deprecation:deprecation -> ty_ml list -> unit |