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=41cc72738c7562e638cc146d0596bdad6eac061c;hpb=218c0062f93dd3221b0266cfbc26fd9cf787ad18;p=helm.git

diff --git a/helm/ocaml/cic_omdoc/eta_fixing.ml b/helm/ocaml/cic_omdoc/eta_fixing.ml
index 41cc72738..68dec37d6 100644
--- a/helm/ocaml/cic_omdoc/eta_fixing.ml
+++ b/helm/ocaml/cic_omdoc/eta_fixing.ml
@@ -242,7 +242,7 @@ let eta_fix metasenv context t =
                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 = 
@@ -299,7 +299,7 @@ let eta_fix metasenv context t =
         let ty =
 	  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