diff options
Diffstat (limited to 'plugins/ltac/tacentries.mli')
| -rw-r--r-- | plugins/ltac/tacentries.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/ltac/tacentries.mli b/plugins/ltac/tacentries.mli index 969c118fb..069504473 100644 --- a/plugins/ltac/tacentries.mli +++ b/plugins/ltac/tacentries.mli @@ -45,7 +45,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 -> +val add_ml_tactic_notation : ml_tactic_name -> level:int -> 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. *) |