diff options
Diffstat (limited to 'ltac/extraargs.mli')
| -rw-r--r-- | ltac/extraargs.mli | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/ltac/extraargs.mli b/ltac/extraargs.mli index 4d1d8ba7fe..0cf77935c2 100644 --- a/ltac/extraargs.mli +++ b/ltac/extraargs.mli @@ -16,6 +16,8 @@ val wit_orient : bool Genarg.uniform_genarg_type val orient : bool Pcoq.Gram.entry val pr_orient : bool -> Pp.std_ppcmds +val wit_rename : (Id.t * Id.t) Genarg.uniform_genarg_type + val occurrences : (int list or_var) Pcoq.Gram.entry val wit_occurrences : (int list or_var, int list or_var, int list) Genarg.genarg_type val pr_occurrences : int list or_var -> Pp.std_ppcmds @@ -38,6 +40,11 @@ val wit_lconstr : Tacexpr.glob_constr_and_expr, Constr.t) Genarg.genarg_type +val wit_casted_constr : + (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 |