Improvements in generalized rewriting:

- support a new strategy: reduction using any of the allowed reduction
operators. This strategy does _not_ make the proof size grow.
- support rewriting under arbitrary [match with] using a folding
strategy. We fold matches to applications of registered [case]
combinators and let the user declare the Proper instances for them.
- fix the lemma application strategy to correctly report when no
progress has been made (avoids loop when repeateadly rewriting with
convertible terms).


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12844 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 3 insertions, 3 deletions

diff --git a/plugins/setoid_ring/newring.ml4 b/plugins/setoid_ring/newring.ml4
index cd9137fd0..490ae89db 100644
--- a/plugins/setoid_ring/newring.ml4
+++ b/plugins/setoid_ring/newring.ml4
@@ -531,7 +531,7 @@ let ring_equality (r,add,mul,opp,req) =
 	  (setoid,op_morph)
     | _ ->
 	let setoid = setoid_of_relation (Global.env ()) r req in
-	let signature = [Some (r,req);Some (r,req)],Some(r,req) in
+	let signature = [Some (r,Some req);Some (r,Some req)],Some(r,Some req) in
 	let add_m, add_m_lem =
 	  try Rewrite.default_morphism signature add
           with Not_found ->
@@ -544,7 +544,7 @@ let ring_equality (r,add,mul,opp,req) =
           match opp with
             | Some opp ->
 		(let opp_m,opp_m_lem =
-		  try Rewrite.default_morphism ([Some(r,req)],Some(r,req)) opp
+		  try Rewrite.default_morphism ([Some(r,Some req)],Some(r,Some req)) opp
 		  with Not_found ->
                     error "ring opposite should be declared as a morphism" in
 		let op_morph =
@@ -1031,7 +1031,7 @@ let field_equality r inv req =
         mkApp((Coqlib.build_coq_eq_data()).congr,[|r;r;inv|])
     | _ ->
 	let _setoid = setoid_of_relation (Global.env ()) r req in
-	let signature = [Some (r,req)],Some(r,req) in
+	let signature = [Some (r,Some req)],Some(r,Some req) in
 	let inv_m, inv_m_lem =
 	  try Rewrite.default_morphism signature inv
           with Not_found ->