diff options
Diffstat (limited to 'ltac/extraargs.mli')
| -rw-r--r-- | ltac/extraargs.mli | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/ltac/extraargs.mli b/ltac/extraargs.mli index 0cf77935c..b12187e18 100644 --- a/ltac/extraargs.mli +++ b/ltac/extraargs.mli @@ -71,3 +71,8 @@ val pr_by_arg_tac : val retroknowledge_field : Retroknowledge.field Pcoq.Gram.entry val wit_retroknowledge_field : (Retroknowledge.field, unit, unit) Genarg.genarg_type + +val wit_in_clause : + (Id.t Loc.located Locus.clause_expr, + Id.t Loc.located Locus.clause_expr, + Id.t Locus.clause_expr) Genarg.genarg_type |