diff options
| author | sacerdot | 2004-09-30 10:56:57 +0000 |
|---|---|---|
| committer | sacerdot | 2004-09-30 10:56:57 +0000 |
| commit | f208cfc23dc997fd0409a9309628bc1804287d7d (patch) | |
| tree | 36d682667cebf7441ff09fe363a82f88d9a7500c /tactics | |
| parent | 59733284601775fd4437ab73eab9c9875c3a6b5b (diff) | |
setoid_replace E1 with E2
now replaces E1 with E2 either generating the goal E1 R E2
or the goal E2 R E1 (as expected).
Note: the relation R is guessed when more than one is applicable.
This is not very nice, since it can guess the wrong one.
Since making the tactic compute R requires much code refactoring, I
would suggest the user to always use cutrewrite in place of setoid_rewrite.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6162 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/setoid_replace.ml | 11 |
1 files changed, 8 insertions, 3 deletions
diff --git a/tactics/setoid_replace.ml b/tactics/setoid_replace.ml index 3e605b17f6..7e22f8e5ee 100644 --- a/tactics/setoid_replace.ml +++ b/tactics/setoid_replace.ml @@ -1349,12 +1349,17 @@ let setoid_replace c1 c2 ~new_goals gl = Relation sa -> sa | Leibniz _ -> raise Use_replace in - let eq = mkApp (relation.rel_aeq, [| c1 ; c2 |]) in + let eq_left_to_right = mkApp (relation.rel_aeq, [| c1 ; c2 |]) in + let eq_right_to_left = mkApp (relation.rel_aeq, [| c2 ; c1 |]) in + let replace dir eq = tclTHENS (assert_tac false Anonymous eq) [onLastHyp (fun id -> tclTHEN - (general_s_rewrite true (mkVar id) ~new_goals) + (general_s_rewrite dir (mkVar id) ~new_goals) (clear [id])); - Tacticals.tclIDTAC] gl + Tacticals.tclIDTAC] + in + tclORELSE + (replace true eq_left_to_right) (replace false eq_right_to_left) gl with Use_replace -> (!replace c1 c2) gl |