diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-04-15 18:26:28 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-04-24 19:16:33 +0200 |
| commit | b090942f20ac8854bf227698d31ca1efec492c47 (patch) | |
| tree | 61cdc57146c4151fa743de9b3c2ab59b11722f92 /ltac/tacentries.mli | |
| parent | f3515efc26a693f4c525ad91c37c982f4c96e6ec (diff) | |
Higher-level API for tactic notations.
Diffstat (limited to 'ltac/tacentries.mli')
| -rw-r--r-- | ltac/tacentries.mli | 11 |
1 files changed, 6 insertions, 5 deletions
diff --git a/ltac/tacentries.mli b/ltac/tacentries.mli index 0f4bb2530..cd9f430cb 100644 --- a/ltac/tacentries.mli +++ b/ltac/tacentries.mli @@ -13,14 +13,15 @@ type 'a grammar_tactic_prod_item_expr = | TacTerm of string | TacNonTerm of Loc.t * 'a * Names.Id.t -(** Adding a tactic notation in the environment *) - val add_tactic_notation : - locality_flag * int * (string * string option) grammar_tactic_prod_item_expr list * raw_tactic_expr -> - unit + locality_flag -> int -> (string * string option) 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] *) val add_ml_tactic_notation : ml_tactic_name -> - Tacexpr.raw_tactic_expr Egramml.grammar_prod_item list list -> unit + Genarg.ArgT.any Extend.user_symbol grammar_tactic_prod_item_expr list list -> unit val register_ltac : bool -> Vernacexpr.tacdef_body list -> unit |