diff options
| author | sacerdot | 2004-09-29 14:51:29 +0000 |
|---|---|---|
| committer | sacerdot | 2004-09-29 14:51:29 +0000 |
| commit | a33f08f8060f99a6ccc33f049ea3c52fc028b3c0 (patch) | |
| tree | 60aa93c22efed3c76be3eee3fc3a1cd82cfc7eda /contrib | |
| parent | c3a4c70688db675c79878df33b4210a4315baf54 (diff) | |
New syntax
"setoid_rewrite dir term generate side conditions constr_list"
to specify a list of side conditions that must be a subset of the generated
new goals. Used to disambiguate in case of multiple set of generated
side conditions.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6157 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib')
| -rw-r--r-- | contrib/ring/ring.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/contrib/ring/ring.ml b/contrib/ring/ring.ml index 9221ed68fd..d72ee19e2c 100644 --- a/contrib/ring/ring.ml +++ b/contrib/ring/ring.ml @@ -806,8 +806,8 @@ let raw_polynom th op lc gl = c'''i; ci; c'i_eq_c''i |])))) (tclTHEN (tclORELSE - (Setoid_replace.setoid_replace ci c'''i) - (Setoid_replace.setoid_replace c'''i ci)) + (Setoid_replace.setoid_replace ci c'''i ~new_goals:[]) + (Setoid_replace.setoid_replace c'''i ci ~new_goals:[])) (tclTHEN (tclTRY (h_exact c'i_eq_c''i)) tac))) |