diff options
| author | Pierre-Marie Pédrot | 2020-05-11 12:18:40 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-05-11 12:18:40 +0200 |
| commit | 0abac9befe6f165dd7829430a229192e6cb18453 (patch) | |
| tree | 744c8d39701f3226c4fc3bdbaafc10bada0b2de7 /plugins/ltac/extraargs.mli | |
| parent | aab47903fb2d3e0085b03d5ade94f4ae644cd76c (diff) | |
| parent | 6e4ebb2dbaa2cb9eb70ce205386bee08c80aaa00 (diff) | |
Merge PR #12129: Add a `with_strategy` tactic
Ack-by: Zimmi48
Ack-by: ejgallego
Ack-by: herbelin
Ack-by: ppedrot
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 |