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 b867793375c42beb657112d508256d8ab66e79b4..68dec37d6b04230f1468665e0a6f77516ccdb365 100644 (file)
--- 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