diff options
Diffstat (limited to 'ltac/tacentries.ml')
| -rw-r--r-- | ltac/tacentries.ml | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/ltac/tacentries.ml b/ltac/tacentries.ml index fc3dfc78d..91eaa8522 100644 --- a/ltac/tacentries.ml +++ b/ltac/tacentries.ml @@ -23,6 +23,9 @@ type 'a grammar_tactic_prod_item_expr = | TacTerm of string | TacNonTerm of Loc.t * 'a * Names.Id.t +type raw_argument = string * string option +type argument = Genarg.ArgT.any Extend.user_symbol + (**********************************************************************) (* Interpret entry names of the form "ne_constr_list" as entry keys *) |