aboutsummaryrefslogtreecommitdiffhomepage
path: root/ide/coq_commands.ml
diff options
context:
space:
mode:
authorGravatar sacerdot <sacerdot@85f007b7-540e-0410-9357-904b9bb8a0f7>2004-09-03 09:31:04 +0000
committerGravatar sacerdot <sacerdot@85f007b7-540e-0410-9357-904b9bb8a0f7>2004-09-03 09:31:04 +0000
commit8fb7ef8984de20f1b6adbc5f438bd6cfcf4d1ed0 (patch)
tree836b8ee133c554bdeb732cddf45c0795e4d792b1 /ide/coq_commands.ml
parentc0d7769b366e387ed9e00b05870991c4c9440f41 (diff)
The old implementation of (setoid_replace c1 with c2) used to replace
either c1 with c2 or c2 with c1 (if c1 did not occur in the goal). The new implementation will not do it. Thus I am replacing every occurrence of (setoid_replace c1 with c2) with (setoid_replace c1 with c2 || setoid_replace c2 with c1). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6047 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'ide/coq_commands.ml')
0 files changed, 0 insertions, 0 deletions