X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcic_acic%2Feta_fixing.ml;h=9ebd48b8b05f2233b72dc741f098e92ebc61f407;hb=f9abd21eb0d26cf9b632af4df819225be4d091e3;hp=90f33d0811bf39d8d8e462b21fe0bba50a715a5d;hpb=cc23f034c9419186602d9250456241f2eba90d7c;p=helm.git

diff --git a/helm/software/components/cic_acic/eta_fixing.ml b/helm/software/components/cic_acic/eta_fixing.ml
index 90f33d081..9ebd48b8b 100644
--- a/helm/software/components/cic_acic/eta_fixing.ml
+++ b/helm/software/components/cic_acic/eta_fixing.ml
@@ -211,7 +211,7 @@ let eta_fix metasenv context t =
        let tl' =  List.map (eta_fix' context) tl in 
        let ty,_ = 
          CicTypeChecker.type_of_aux' metasenv context he 
-           CicUniv.empty_ugraph 
+           CicUniv.oblivion_ugraph 
        in
        fix_according_to_type ty (eta_fix' context he) tl'
 (*
@@ -240,7 +240,7 @@ let eta_fix metasenv context t =
        let term' = eta_fix' context term in
        let patterns' = List.map (eta_fix' context) patterns in
        let inductive_types,noparams =
-	 let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
+	 let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in
            (match o with
                Cic.Constant _ -> assert false
              | Cic.Variable _ -> assert false
@@ -261,7 +261,7 @@ let eta_fix metasenv context t =
           else 
 	    let term_type,_ = 
               CicTypeChecker.type_of_aux' metasenv context term
-		CicUniv.empty_ugraph 
+		CicUniv.oblivion_ugraph 
             in
             (match term_type with
                C.Appl (hd::params) -> 
@@ -300,7 +300,7 @@ let eta_fix metasenv context t =
       (fun newsubst (uri,t) ->
         let t' = eta_fix' context t in
         let ty =
-	  let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
+	  let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in
             match o with
 		Cic.Variable (_,_,ty,_,_) -> 
 		  CicSubstitution.subst_vars newsubst ty