(* $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
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