new cicEnvironment implementation

[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..41cc72738c7562e638cc146d0596bdad6eac061c 100644 (file)
--- a/helm/ocaml/cic_omdoc/eta_fixing.ml
+++ b/helm/ocaml/cic_omdoc/eta_fixing.ml
@@ -237,7 +237,7 @@ 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
@@ -297,7 +297,7 @@ 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,_) -> 
                  CicSubstitution.subst_vars newsubst ty