+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
+