X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2Fsetoids.ml;h=1ef4e483e62f8ec8afdcb6435d54913d3442cdfc;hb=bd3680d6b90f6c8bdda4eb4a915a86a0e806de63;hp=265ef99aa9368e01787b87b771b2012bf331354a;hpb=11b2157bacf59cfc561c2ef6f92ee41ee2c1a006;p=helm.git

diff --git a/helm/software/components/tactics/setoids.ml b/helm/software/components/tactics/setoids.ml
index 265ef99aa..1ef4e483e 100644
--- a/helm/software/components/tactics/setoids.ml
+++ b/helm/software/components/tactics/setoids.ml
@@ -8,6 +8,10 @@
 
 (* $Id: setoid_replace.ml 8900 2006-06-06 14:40:27Z letouzey $ *)
 
+module T = Tacticals
+module RT = ReductionTactics
+module PET = ProofEngineTypes
+
 let default_eq () =
  match LibraryObjects.eq_URI () with
     Some uri -> uri
@@ -1840,6 +1844,11 @@ let setoid_reflexivity_tac =
  in
   ProofEngineTypes.mk_tactic tac
 
+let setoid_reflexivity_tac =
+   let start_tac = RT.whd_tac ~pattern:(PET.conclusion_pattern None) in
+   let fail_tac = T.then_ ~start:start_tac ~continuation:setoid_reflexivity_tac in 
+   T.if_ ~start:setoid_reflexivity_tac ~continuation:T.id_tac ~fail:fail_tac
+
 let setoid_symmetry  =
  let tac status =
   try