diff options
Diffstat (limited to 'ltac/extraargs.mli')
| -rw-r--r-- | ltac/extraargs.mli | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/ltac/extraargs.mli b/ltac/extraargs.mli index 2118e87b11..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 |