Allowing setoid_reflexivity_in to work on quantified hypothesis (bug #1710)

(patch by J. Forest) 



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

1 files changed, 16 insertions, 5 deletions

diff --git a/tactics/setoid_replace.ml b/tactics/setoid_replace.ml
index 176c9c448..36ef9be47 100644
--- a/tactics/setoid_replace.ml
+++ b/tactics/setoid_replace.ml
@@ -1959,11 +1959,22 @@ let setoid_symmetry gl =
   Optimize -> symmetry_red true gl
 
 let setoid_symmetry_in id gl =
- let new_hyp =
-  let _,he,c1,c2 = analyse_hypothesis gl (mkVar id) in
-   mkApp (he, [| c2 ; c1 |])
- in
- cut_replacing id new_hyp (tclTHEN setoid_symmetry) gl
+  let ctype = pf_type_of gl (mkVar id) in
+  let binders,concl = Sign.decompose_prod_assum ctype in
+  let (equiv, args) = decompose_app concl 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 equivalence" 
+  in
+  let others,(c1,c2) = split_last_two args in
+  let he,c1,c2 =  mkApp (equiv, Array.of_list others),c1,c2 in
+  let new_hyp' =  mkApp (he, [| c2 ; c1 |]) in
+  let new_hyp = it_mkProd_or_LetIn new_hyp'  binders in
+  tclTHENS (cut new_hyp)
+    [ intro_replacing id;
+      tclTHENLIST [ intros; setoid_symmetry; apply (mkVar id); assumption ] ]
+    gl
 
 let setoid_transitivity c gl =
  try