diff options
| author | sacerdot | 2004-09-03 09:31:04 +0000 |
|---|---|---|
| committer | sacerdot | 2004-09-03 09:31:04 +0000 |
| commit | 8fb7ef8984de20f1b6adbc5f438bd6cfcf4d1ed0 (patch) | |
| tree | 836b8ee133c554bdeb732cddf45c0795e4d792b1 | |
| parent | c0d7769b366e387ed9e00b05870991c4c9440f41 (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
| -rw-r--r-- | contrib/ring/ring.ml | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/contrib/ring/ring.ml b/contrib/ring/ring.ml index 178b866de0..9221ed68fd 100644 --- a/contrib/ring/ring.ml +++ b/contrib/ring/ring.ml @@ -805,7 +805,9 @@ let raw_polynom th op lc gl = (unbox th.th_setoid_th); c'''i; ci; c'i_eq_c''i |])))) (tclTHEN - (Setoid_replace.setoid_replace ci c'''i) + (tclORELSE + (Setoid_replace.setoid_replace ci c'''i) + (Setoid_replace.setoid_replace c'''i ci)) (tclTHEN (tclTRY (h_exact c'i_eq_c''i)) tac))) |