diff options
| author | Hugo Herbelin | 2014-08-17 17:28:19 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2014-08-18 18:56:38 +0200 |
| commit | ca36da7eaa33f07c0bc9163fa10b017478c2ee0f (patch) | |
| tree | 3891ff920186e9a150daf96073e9e3bbaadb47bc /tactics/equality.mli | |
| parent | b6c3f54d04ce441ac68ffabfca69c18847707518 (diff) | |
Slight simplification of naming of tactics in equality.ml (hopefully).
Isolating a core tactic in replace, shareable to cutrewrite.
Diffstat (limited to 'tactics/equality.mli')
| -rw-r--r-- | tactics/equality.mli | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/tactics/equality.mli b/tactics/equality.mli index 2993c8d3a4..4899cd91d5 100644 --- a/tactics/equality.mli +++ b/tactics/equality.mli @@ -41,7 +41,7 @@ val rewriteRL : ?tac:(unit Proofview.tactic * conditions) -> constr -> unit Pro (* Warning: old [general_rewrite_in] is now [general_rewrite_bindings_in] *) -val general_rewrite_clause : +val general_setoid_rewrite_clause : (Id.t option -> orientation -> occurrences -> constr with_bindings -> new_goals:constr list -> unit Proofview.tactic) Hook.t @@ -57,13 +57,13 @@ val general_rewrite_in : orientation -> occurrences -> freeze_evars_flag -> dep_proof_flag -> ?tac:(unit Proofview.tactic * conditions) -> Id.t -> constr -> evars_flag -> unit Proofview.tactic -val general_multi_rewrite : +val general_rewrite_clause : orientation -> evars_flag -> ?tac:(unit Proofview.tactic * conditions) -> constr with_bindings -> clause -> unit Proofview.tactic type delayed_open_constr_with_bindings = env -> evar_map -> evar_map * constr with_bindings -val general_multi_multi_rewrite : +val general_multi_rewrite : evars_flag -> (bool * multi * clear_flag * delayed_open_constr_with_bindings) list -> clause -> (unit Proofview.tactic * conditions) option -> unit Proofview.tactic @@ -114,10 +114,10 @@ val subst : Id.t list -> unit Proofview.tactic val subst_all : ?flags:subst_tactic_flags -> unit -> unit Proofview.tactic (* Replace term *) -(* [replace_multi_term dir_opt c cl] +(* [replace_term dir_opt c cl] perfoms replacement of [c] by the first value found in context (according to [dir] if given to get the rewrite direction) in the clause [cl] *) -val replace_multi_term : bool option -> constr -> clause -> unit Proofview.tactic +val replace_term : bool option -> constr -> clause -> unit Proofview.tactic val set_eq_dec_scheme_kind : mutual scheme_kind -> unit |