diff options
| author | sacerdot | 2004-09-30 16:26:35 +0000 |
|---|---|---|
| committer | sacerdot | 2004-09-30 16:26:35 +0000 |
| commit | 8a00bdd6d838f65601ed9006671a8afcb9a1890d (patch) | |
| tree | 2cb394f0694d3f3f8deb7485719a83c45c89bee3 /tactics/setoid_replace.mli | |
| parent | 03a61c73a53ce64b8334cefd0df9041bf891d15b (diff) | |
New tactic [setoid_]rewrite ... in ... [generate side conditions ...].
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6165 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics/setoid_replace.mli')
| -rw-r--r-- | tactics/setoid_replace.mli | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/tactics/setoid_replace.mli b/tactics/setoid_replace.mli index d815954ec4..3b71708b4a 100644 --- a/tactics/setoid_replace.mli +++ b/tactics/setoid_replace.mli @@ -11,7 +11,7 @@ open Term open Proof_type open Topconstr - +open Names type morphism_signature = (bool option * constr_expr) list * constr_expr @@ -28,6 +28,8 @@ val setoid_replace : constr option -> constr -> constr -> new_goals:constr list -> tactic val general_s_rewrite : bool -> constr -> new_goals:constr list -> tactic +val general_s_rewrite_in : + identifier -> bool -> constr -> new_goals:constr list -> tactic val add_relation : constr_expr -> constr_expr -> constr_expr option -> constr_expr option -> unit |