Fix bug reported by Mark Dickinson on Coq-Club about [setoid_rewrite] not

reducing the type of the given lemma.


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

1 files changed, 30 insertions, 22 deletions

diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4
index 33bc17624..21be8296c 100644
--- a/tactics/class_tactics.ml4
+++ b/tactics/class_tactics.ml4
@@ -69,10 +69,10 @@ open Auto
 let e_give_exact flags c gl = 
   let t1 = (pf_type_of gl c) and t2 = pf_concl gl in 
     if occur_existential t1 or occur_existential t2 then 
-      tclTHEN (Clenvtac.unify (* ~flags *) t1) (exact_check c) gl
+      tclTHEN (Clenvtac.unify (* ~flags *) t1) (exact_no_check c) gl
     else exact_check c gl
 (*   let t1 = (pf_type_of gl c) in *)
-(*     tclTHEN (Clenvtac.unify ~flags t1) (exact_check c) gl *)
+(*     tclTHEN (Clenvtac.unify ~flags t1) (exact_no_check c) gl *)
       
 let assumption flags id = e_give_exact flags (mkVar id)
 
@@ -752,24 +752,32 @@ let evd_convertible env evd x y =
   
 let decompose_setoid_eqhyp env sigma c left2right =
   let ctype = Typing.type_of env sigma c in
-  let eqclause = Clenv.mk_clenv_from_env env sigma None (c,ctype) in
-  let (equiv, args) = decompose_app (Clenv.clenv_type eqclause) in
-  let rec split_last_two = function
-    | [c1;c2] -> [],(c1, c2)
-    | x::y::z ->
-	let l,res = split_last_two (y::z) in x::l, res
-    | _ -> error "The term provided is not an applied relation." in
-  let others,(c1,c2) = split_last_two args in
-  let ty1, ty2 = 
-    Typing.mtype_of env eqclause.evd c1, Typing.mtype_of env eqclause.evd c2
+  let find_rel ty = 
+    let eqclause = Clenv.mk_clenv_from_env env sigma None (c,ty) in
+    let (equiv, args) = decompose_app (Clenv.clenv_type eqclause) in
+    let rec split_last_two = function
+      | [c1;c2] -> [],(c1, c2)
+      | x::y::z ->
+	  let l,res = split_last_two (y::z) in x::l, res
+      | _ -> error "The term provided is not an applied relation." in
+    let others,(c1,c2) = split_last_two args in
+    let ty1, ty2 = 
+      Typing.mtype_of env eqclause.evd c1, Typing.mtype_of env eqclause.evd c2
+    in
+      if not (evd_convertible env eqclause.evd ty1 ty2) then None
+      else
+	Some { cl=eqclause; prf=(Clenv.clenv_value eqclause);
+	       car=ty1; rel=mkApp (equiv, Array.of_list others);
+	       l2r=left2right; c1=c1; c2=c2; c=Some c; abs=None }
   in
-    if not (evd_convertible env eqclause.evd ty1 ty2) then
-      error "The term does not end with an applied homogeneous relation."
-    else
-      { cl=eqclause; prf=(Clenv.clenv_value eqclause);
-	car=ty1; rel=mkApp (equiv, Array.of_list others);
-	l2r=left2right; c1=c1; c2=c2; c=Some c; abs=None }
-
+    match find_rel ctype with
+    | Some c -> c
+    | None -> 
+	let ctx,t' = Reductionops.splay_prod_assum env sigma ctype in (* Search for underlying eq *)
+	match find_rel (it_mkProd_or_LetIn t' ctx) with
+	| Some c -> c
+	| None -> error "The term does not end with an applied homogeneous relation."
+	    
 let rewrite_unif_flags = {
   Unification.modulo_conv_on_closed_terms = None;
   Unification.use_metas_eagerly = true;
@@ -1506,7 +1514,8 @@ let add_morphism_infer m n =
 	    Command.start_proof instance_id kind instance 
 	      (fun _ -> function
 		  Libnames.ConstRef cst -> 
-		    add_instance (Typeclasses.new_instance (Lazy.force morphism_class) None false cst);
+		    add_instance (Typeclasses.new_instance 
+				     (Lazy.force morphism_class) None false cst);
 		    declare_projection n instance_id (ConstRef cst)
 		| _ -> assert false);
 	    Pfedit.by (Tacinterp.interp <:tactic< Coq.Classes.SetoidTactics.add_morphism_tactic>>)) ();
@@ -1523,8 +1532,7 @@ let add_morphism binders m s n =
   in	  
   let tac = Tacinterp.interp <:tactic<add_morphism_tactic>> in
     ignore(new_instance binders instance (CRecord (dummy_loc,None,[]))
-	      ~generalize:false ~tac ~hook:(fun cst -> declare_projection n instance_id (ConstRef cst))
-	      None)
+	      ~generalize:false ~tac ~hook:(fun cst -> declare_projection n instance_id (ConstRef cst)) None)
 
 VERNAC COMMAND EXTEND AddSetoid1
    [ "Add" "Setoid" constr(a) constr(aeq) constr(t) "as" ident(n) ] ->