(* $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
let argsno = List.length args' - rel.rel_quantifiers_no in
let args1 = list_sub args' 0 argsno in
let args2 = list_sub args' argsno rel.rel_quantifiers_no in
- if fst (CicReduction.are_convertible [] rel.rel_a (Cic.Appl (he'::args1)) CicUniv.empty_ugraph) then
+ if fst (CicReduction.are_convertible [] rel.rel_a (Cic.Appl (he'::args1))
+ CicUniv.oblivion_ugraph) then
args2
else
raise_error rel.rel_quantifiers_no
| _ ->
- if rel.rel_quantifiers_no = 0 && fst (CicReduction.are_convertible [] rel.rel_a t CicUniv.empty_ugraph) then
+ if rel.rel_quantifiers_no = 0 && fst (CicReduction.are_convertible []
+ rel.rel_a t CicUniv.oblivion_ugraph) then
[]
else
begin
(*COQ
let evars,args,instantiated_rel_a =
- let ty = CicTypeChecker.type_of_aux' [] [] rel.rel_a CicUniv.empty_ugraph in
+ let ty = CicTypeChecker.type_of_aux' [] [] rel.rel_a
+ CicUniv.oblivion_ugraph in
let evd = Evd.create_evar_defs Evd.empty in
let evars,args,concl =
Clenv.clenv_environments_evars env evd
let unify_relation_class_carrier_with_type env rel t =
match rel with
Leibniz (Some t') ->
- if fst (CicReduction.are_convertible [] t t' CicUniv.empty_ugraph) then
+ if fst (CicReduction.are_convertible [] t t' CicUniv.oblivion_ugraph) then
rel
else
raise (ProofEngineTypes.Fail (lazy
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
let hyp = CicSubstitution.subst (CicSubstitution.lift 1 c2) hyp in
(* Since CicSubstitution.subst has killed Rel 1 and decreased the other Rels,
Rel 1 is now coding for c2, we can build the let-in factorizing c2 *)
- Cic.LetIn (Cic.Anonymous,c2,hyp)
+ Cic.LetIn (Cic.Anonymous,c2,assert false,hyp)
in
let new_hyp = (*COQ Termops.replace_term c1 c2 hyp*) assert false in
let oppdir = opposite_direction direction in
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