diff options
Diffstat (limited to 'plugins/ltac/extraargs.mli')
| -rw-r--r-- | plugins/ltac/extraargs.mli | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/plugins/ltac/extraargs.mli b/plugins/ltac/extraargs.mli index fbdb7c0032..e52bf55f71 100644 --- a/plugins/ltac/extraargs.mli +++ b/plugins/ltac/extraargs.mli @@ -78,3 +78,7 @@ val wit_in_clause : (lident Locus.clause_expr, lident Locus.clause_expr, Id.t Locus.clause_expr) Genarg.genarg_type + +val wit_strategy_level : Conv_oracle.level Genarg.uniform_genarg_type + +val wit_strategy_level_or_var : (Conv_oracle.level Locus.or_var, Conv_oracle.level Locus.or_var, Conv_oracle.level) Genarg.genarg_type |