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/setoid_replace.mli | |
| 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/setoid_replace.mli')
0 files changed, 0 insertions, 0 deletions