diff options
Diffstat (limited to 'tactics/extraargs.mli')
| -rw-r--r-- | tactics/extraargs.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/extraargs.mli b/tactics/extraargs.mli index cd4d777d6..1367f7032 100644 --- a/tactics/extraargs.mli +++ b/tactics/extraargs.mli @@ -26,7 +26,7 @@ val occurrences_of : int list -> Locus.occurrences val wit_glob : (constr_expr, - Genarg.glob_constr_and_expr, + Tacexpr.glob_constr_and_expr, Tacinterp.interp_sign * glob_constr) Genarg.genarg_type val glob : constr_expr Pcoq.Gram.entry |