X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2Fsetoids.ml;h=d85df1c4b1e2de3b215524257ee15d71b2ec9474;hb=ee242468b221c64b25c99b52110fe00380f4eebe;hp=7d0e958cc40ce059e980a1b3d3a467eb2633756a;hpb=c6cc2a7227d6750076f591a62d7b1896ebf1ebfa;p=helm.git

diff --git a/helm/software/components/tactics/setoids.ml b/helm/software/components/tactics/setoids.ml
index 7d0e958cc..d85df1c4b 100644
--- a/helm/software/components/tactics/setoids.ml
+++ b/helm/software/components/tactics/setoids.ml
@@ -646,18 +646,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 +685,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
@@ -1745,7 +1748,7 @@ let relation_rewrite_in id c1 c2 (direction,eqclause) ~new_goals gl =
    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