diff options
| author |  sacerdot <sacerdot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2005-02-02 21:13:43 +0000 |
|---|---|---|
| committer | sacerdot <sacerdot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2005-02-02 21:13:43 +0000 |
| commit | 4bf699dc783072ee4c1e641e018474fbbf710e99 (patch) | |
| tree | 4dca133605b51a88793f094baacc5697f7882447 | |
| parent | 708b76785e9354565de5445749e81bb680ed6098 (diff) | |
setoid_rewrite t; [tac]
now used in place of
setoid_replace ... with ... ; try (exact t) ; tac
The new stricter version closes a bug reported by Pierre Letouzey on coqdev.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6661 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | contrib/ring/ring.ml | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/contrib/ring/ring.ml b/contrib/ring/ring.ml index 1eb4783d1..876020dda 100644 --- a/contrib/ring/ring.ml +++ b/contrib/ring/ring.ml @@ -805,13 +805,13 @@ let raw_polynom th op lc gl = [| th.th_a; (unbox th.th_equiv); (unbox th.th_setoid_th); c'''i; ci; c'i_eq_c''i |])))) - (tclTHEN + (tclTHENS (tclORELSE - (Setoid_replace.setoid_replace None ci c'''i ~new_goals:[]) - (Setoid_replace.setoid_replace None c'''i ci ~new_goals:[])) - (tclTHEN - (tclTRY (h_exact c'i_eq_c''i)) - tac))) + (Setoid_replace.general_s_rewrite true c'i_eq_c''i + ~new_goals:[]) + (Setoid_replace.general_s_rewrite false c'i_eq_c''i + ~new_goals:[])) + [tac])) else (tclORELSE (tclORELSE |