aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/extraargs.mli
diff options
context:
space:
mode:
Diffstat (limited to 'tactics/extraargs.mli')
-rw-r--r--tactics/extraargs.mli2
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/extraargs.mli b/tactics/extraargs.mli
index 7c206d95c..7df845e4b 100644
--- a/tactics/extraargs.mli
+++ b/tactics/extraargs.mli
@@ -47,7 +47,7 @@ val by_arg_tac : Tacexpr.raw_tactic_expr option Pcoq.Gram.entry
val wit_by_arg_tac :
(raw_tactic_expr option,
glob_tactic_expr option,
- glob_tactic_expr option) Genarg.genarg_type
+ Genarg.Val.t option) Genarg.genarg_type
val pr_by_arg_tac :
(int * Ppextend.parenRelation -> raw_tactic_expr -> Pp.std_ppcmds) ->