Minor fixes on setoid rewriting. Now uses definitions of [relation] and

[id] instead of their expansions. Seems to slow things down a bit
(1s. on Ring_polynom).


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

2 files changed, 27 insertions, 28 deletions

diff --git a/contrib/setoid_ring/newring.ml4 b/contrib/setoid_ring/newring.ml4
index bce41b9b5..6ed79f23b 100644
--- a/contrib/setoid_ring/newring.ml4
+++ b/contrib/setoid_ring/newring.ml4
@@ -527,7 +527,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,req);Some (r,req)],Some(r,req) in
 	let add_m, add_m_lem =
 	  try Class_tactics.default_morphism signature add
           with Not_found ->
@@ -540,7 +540,7 @@ let ring_equality (r,add,mul,opp,req) =
           match opp with
             | Some opp ->
 		(let opp_m,opp_m_lem =
-		  try Class_tactics.default_morphism (List.tl signature) opp
+		  try Class_tactics.default_morphism ([Some(r,req)],Some(r,req)) opp
 		  with Not_found ->
                     error "ring opposite should be declared as a morphism" in
 		let op_morph =
@@ -1035,7 +1035,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,req)],Some(r,req) in
 	let inv_m, inv_m_lem =
 	  try Class_tactics.default_morphism signature inv
           with Not_found ->
diff --git a/contrib/subtac/subtac_coercion.ml b/contrib/subtac/subtac_coercion.ml
index e6150710e..0f9331ff5 100644
--- a/contrib/subtac/subtac_coercion.ml
+++ b/contrib/subtac/subtac_coercion.ml
@@ -524,7 +524,6 @@ module Coercion = struct
 	  (isevars, cj)
 
   let inh_conv_coerces_to loc env isevars t ((abs, t') as _tycon) =
-    isevars
 (*     (try *)
 (*        trace (str "Subtac_coercion.inh_conv_coerces_to called for " ++ *)
 (* 	      Termops.print_constr_env env t ++ str " and "++ spc () ++ *)
@@ -532,30 +531,30 @@ module Coercion = struct
 (* 	      Evd.pr_evar_defs isevars ++ str " in env: " ++ spc () ++ *)
 (* 	      Termops.print_env env); *)
 (*      with _ -> ()); *)
-(*     let nabsinit, nabs = *)
-(*       match abs with *)
-(* 	  None -> 0, 0 *)
-(* 	| Some (init, cur) -> init, cur *)
-(*     in *)
-(*       (\* a little more effort to get products is needed *\) *)
-(*       try let rels, rng = decompose_prod_n nabs t in *)
-(* 	(\* The final range free variables must have been replaced by evars, we accept only that evars *)
-(* 	   in rng are applied to free vars. *\) *)
-(* 	if noccur_with_meta 0 (succ nabsinit) rng then ( *)
-(* (\* 	  trace (str "No occur between 0 and " ++ int (succ nabsinit)); *\) *)
-(* 	  let env', t, t' = *)
-(* 	    let env' = List.fold_right (fun (n, t) env -> push_rel (n, None, t) env) rels env in *)
-(* 	      env', rng, lift nabs t' *)
-(* 	  in *)
-(* 	    try *)
-(* 	      pi1 (try inh_conv_coerce_to_fail loc env' isevars None t t' *)
-(* 		   with NoCoercion -> *)
-(* 		     coerce_itf loc env' isevars None t t') *)
-(* 	    with NoSubtacCoercion -> *)
-(* 	      let sigma = evars_of isevars in *)
-(* 		error_cannot_coerce env' sigma (t, t')) *)
-(* 	else isevars *)
-(*       with _ -> isevars *)
+    let nabsinit, nabs =
+      match abs with
+	  None -> 0, 0
+	| Some (init, cur) -> init, cur
+    in
+      (* a little more effort to get products is needed *)
+      try let rels, rng = decompose_prod_n nabs t in
+	(* The final range free variables must have been replaced by evars, we accept only that evars
+	   in rng are applied to free vars. *)
+	if noccur_with_meta 0 (succ nabsinit) rng then (
+(* 	  trace (str "No occur between 0 and " ++ int (succ nabsinit)); *)
+	  let env', t, t' =
+	    let env' = List.fold_right (fun (n, t) env -> push_rel (n, None, t) env) rels env in
+	      env', rng, lift nabs t'
+	  in
+	    try
+	      pi1 (try inh_conv_coerce_to_fail loc env' isevars None t t'
+		   with NoCoercion ->
+		     coerce_itf loc env' isevars None t t')
+	    with NoSubtacCoercion ->
+	      let sigma = evars_of isevars in
+		error_cannot_coerce env' sigma (t, t'))
+	else isevars
+      with _ -> isevars
 (*  	trace (str "decompose_prod_n failed"); *)
 (*  	raise (Invalid_argument "Subtac_coercion.inh_conv_coerces_to") *)
 end