X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_omdoc%2Feta_fixing.ml;h=68dec37d6b04230f1468665e0a6f77516ccdb365;hb=97c2d258a5c524eb5c4b85208899d80751a2c82f;hp=b867793375c42beb657112d508256d8ab66e79b4;hpb=31851952e1cc2db59168c5fd6f6093d9bc37ea86;p=helm.git

diff --git a/helm/ocaml/cic_omdoc/eta_fixing.ml b/helm/ocaml/cic_omdoc/eta_fixing.ml
index b86779337..68dec37d6 100644
--- a/helm/ocaml/cic_omdoc/eta_fixing.ml
+++ b/helm/ocaml/cic_omdoc/eta_fixing.ml
@@ -237,12 +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 =
-	 let o,_ = CicEnvironment.get_obj uri CicUniv.empty_ugraph in
+	 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 = 
@@ -297,9 +297,9 @@ let eta_fix metasenv context t =
       (fun newsubst (uri,t) ->
         let t' = eta_fix' context t in
         let ty =
-	  let o,_ = CicEnvironment.get_obj uri CicUniv.empty_ugraph in
+	  let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
             match o with
-		Cic.Variable (_,_,ty,_) -> 
+		Cic.Variable (_,_,ty,_,_) -> 
 		  CicSubstitution.subst_vars newsubst ty
               | _ ->  raise ReferenceToNonVariable 
 	in