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

diff --git a/helm/software/components/tactics/setoids.ml b/helm/software/components/tactics/setoids.ml
index c8ca16317..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
@@ -646,18 +650,21 @@ let unify_relation_carrier_with_type env rel t =
       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
@@ -682,7 +689,7 @@ let unify_relation_carrier_with_type env rel t =
 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
@@ -955,7 +962,7 @@ let int_add_relation id a aeq refl sym trans =
      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
@@ -976,7 +983,7 @@ let int_add_relation id a aeq refl sym trans =
       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
@@ -1837,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