ocaml 3.09 transition

[helm.git] / helm / ocaml / cic_omdoc / eta_fixing.ml

diff --git a/helm/ocaml/cic_omdoc/eta_fixing.ml b/helm/ocaml/cic_omdoc/eta_fixing.ml
index 41cc72738c7562e638cc146d0596bdad6eac061c..68dec37d6b04230f1468665e0a6f77516ccdb365 100644 (file)
--- 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