diff options
| author | Hugo Herbelin | 2014-11-22 18:09:01 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2014-11-22 19:23:32 +0100 |
| commit | b3320b0f942a9f86d5bd1c00876f8816e5c94446 (patch) | |
| tree | 7bb8a6acc55b9711daae22237e55d7c56a05bbab /tactics/rewrite.mli | |
| parent | 250afa5b896a7e8ab5971667e6889ee3a498dfd3 (diff) | |
Attempt to organize and document unification flags of setoid rewrite.
Diffstat (limited to 'tactics/rewrite.mli')
| -rw-r--r-- | tactics/rewrite.mli | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/tactics/rewrite.mli b/tactics/rewrite.mli index 5b82217fd4..f6b2a74ac9 100644 --- a/tactics/rewrite.mli +++ b/tactics/rewrite.mli @@ -65,8 +65,10 @@ val strategy_of_ast : (glob_constr_and_expr, raw_red_expr) strategy_ast -> strat val map_strategy : ('a -> 'b) -> ('c -> 'd) -> ('a, 'c) strategy_ast -> ('b, 'd) strategy_ast +(** Entry point for user-level "rewrite_strat" *) val cl_rewrite_clause_strat : strategy -> Id.t option -> tactic +(** Entry point for user-level "setoid_rewrite" *) val cl_rewrite_clause : interp_sign * (glob_constr_and_expr * glob_constr_and_expr bindings) -> bool -> Locus.occurrences -> Id.t option -> tactic |