(* $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
rel_X_relation_class = Cic.Sort Cic.Prop; (* dummy value, overwritten below *)
rel_Xreflexive_relation_class = Cic.Sort Cic.Prop (* dummy value, overwritten below *)
} in
- let x_relation_class =
+ let _x_relation_class =
let subst =
let len = List.length a_quantifiers_rev in
list_map_i (fun i _ -> Cic.Rel (len - i + 2)) 0 a_quantifiers_rev in
IsDefinition Definition) in
*) () in
let id_precise = id ^ "_precise_relation_class" in
- let xreflexive_relation_class =
+ let _xreflexive_relation_class =
let subst =
let len = List.length a_quantifiers_rev in
list_map_i (fun i _ -> Cic.Rel (len - i)) 0 a_quantifiers_rev
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