X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_omdoc%2Feta_fixing.ml;h=68dec37d6b04230f1468665e0a6f77516ccdb365;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=29d22ccb91062051858e1c55f4619b4433e35e35;hpb=7ec7262cfa317c1962164350361f82a56c5d1826;p=helm.git

diff --git a/helm/ocaml/cic_omdoc/eta_fixing.ml b/helm/ocaml/cic_omdoc/eta_fixing.ml
index 29d22ccb9..68dec37d6 100644
--- a/helm/ocaml/cic_omdoc/eta_fixing.ml
+++ b/helm/ocaml/cic_omdoc/eta_fixing.ml
@@ -206,8 +206,11 @@ let eta_fix metasenv context t =
        (match l' with
            [] -> assert false
          | he::tl ->
-            let ty = CicTypeChecker.type_of_aux' metasenv context he in
-             fix_according_to_type ty he tl
+            let ty,_ = 
+              CicTypeChecker.type_of_aux' metasenv context he 
+		CicUniv.empty_ugraph 
+	    in
+              fix_according_to_type ty he tl
 (*
          C.Const(uri,exp_named_subst)::l'' ->
            let constant_type =
@@ -234,11 +237,12 @@ 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 =
-           (match CicEnvironment.get_obj uri with
+	 let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
+           (match o with
                Cic.Constant _ -> assert false
              | Cic.Variable _ -> assert false
              | Cic.CurrentProof _ -> assert false
-             | Cic.InductiveDefinition (l,_,n) -> l,n 
+             | Cic.InductiveDefinition (l,_,n,_) -> l,n 
            ) in
        let (_,_,_,constructors) = List.nth inductive_types tyno in
        let constructor_types = 
@@ -252,9 +256,10 @@ let eta_fix metasenv context t =
           if noparams = 0 then 
             List.map (fun (_,t) -> t) constructors 
           else 
-	         let term_type = 
-            CicTypeChecker.type_of_aux' metasenv context term
-           in
+	    let term_type,_ = 
+              CicTypeChecker.type_of_aux' metasenv context term
+		CicUniv.empty_ugraph 
+            in
             (match term_type with
                C.Appl (hd::params) -> 
                  let rec first_n n l =
@@ -292,9 +297,12 @@ let eta_fix metasenv context t =
       (fun newsubst (uri,t) ->
         let t' = eta_fix' context t in
         let ty =
-         match CicEnvironment.get_obj uri with
-            Cic.Variable (_,_,ty,_) -> CicSubstitution.subst_vars newsubst ty
-          | _ ->  raise ReferenceToNonVariable in
+	  let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
+            match o with
+		Cic.Variable (_,_,ty,_,_) -> 
+		  CicSubstitution.subst_vars newsubst ty
+              | _ ->  raise ReferenceToNonVariable 
+	in
         let t'' = fix_according_to_type ty t' [] in
          (uri,t'')::newsubst
       ) [] exp_named_subst)