parameter sintax added to axiom statement

[helm.git] / helm / software / components / cic_acic / eta_fixing.ml

diff --git a/helm/software/components/cic_acic/eta_fixing.ml b/helm/software/components/cic_acic/eta_fixing.ml
index 90f33d0811bf39d8d8e462b21fe0bba50a715a5d..9ebd48b8b05f2233b72dc741f098e92ebc61f407 100644 (file)
--- 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