diff options
Diffstat (limited to 'plugins/ltac/tacexpr.mli')
| -rw-r--r-- | plugins/ltac/tacexpr.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/ltac/tacexpr.mli b/plugins/ltac/tacexpr.mli index 9c25a1645..e23992a80 100644 --- a/plugins/ltac/tacexpr.mli +++ b/plugins/ltac/tacexpr.mli @@ -282,7 +282,7 @@ constraint 'a = < > and 'a gen_tactic_fun_ast = - Id.t option list * 'a gen_tactic_expr + Name.t list * 'a gen_tactic_expr constraint 'a = < term:'t; |