diff options
Diffstat (limited to 'tactics/extraargs.mli')
| -rw-r--r-- | tactics/extraargs.mli | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/tactics/extraargs.mli b/tactics/extraargs.mli index f7b379e69e..14aa69875f 100644 --- a/tactics/extraargs.mli +++ b/tactics/extraargs.mli @@ -21,6 +21,8 @@ val wit_occurrences : (int list or_var, int list or_var, int list) Genarg.genarg val pr_occurrences : int list or_var -> Pp.std_ppcmds val occurrences_of : int list -> Locus.occurrences +val wit_natural : int Genarg.uniform_genarg_type + val wit_glob : (constr_expr, Tacexpr.glob_constr_and_expr, @@ -31,6 +33,11 @@ val wit_lglob : Tacexpr.glob_constr_and_expr, Tacinterp.interp_sign * glob_constr) Genarg.genarg_type +val wit_lconstr : + (constr_expr, + Tacexpr.glob_constr_and_expr, + Constr.t) Genarg.genarg_type + val glob : constr_expr Pcoq.Gram.entry val lglob : constr_expr Pcoq.Gram.entry |