new cicEnvironment implementation

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

diff --git a/helm/ocaml/cic_omdoc/cic2content.ml b/helm/ocaml/cic_omdoc/cic2content.ml
index 56459d197278ac902d9e731f7b45647dfead2061..c91eb200b3ed8a0f2ed63d675b6792ceafe1b95f 100644 (file)
--- a/helm/ocaml/cic_omdoc/cic2content.ml
+++ b/helm/ocaml/cic_omdoc/cic2content.ml
@@ -369,7 +369,7 @@ let rec build_subproofs_and_args seed l ~ids_to_inner_types ~ids_to_inner_sorts
                  if sort ="Prop" then 
                     let inductive_types =
                       (let o,_ = 
-                        CicEnvironment.get_obj uri CicUniv.empty_ugraph 
+                        CicEnvironment.get_obj CicUniv.empty_ugraph uri
                       in
                         match o with 
                              Cic.Constant _ -> assert false
@@ -541,7 +541,7 @@ and acic2content seed ?name ~ids_to_inner_sorts ~ids_to_inner_types t =
         else raise Not_a_proof
     | C.AMutCase (id,uri,typeno,ty,te,patterns) ->
         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
@@ -690,7 +690,7 @@ and inductive seed name id li ~ids_to_inner_types ~ids_to_inner_sorts =
         let ind_str = (prefix ^ ".ind") in 
         let ind_uri = UriManager.uri_of_string ind_str in
         let inductive_types,noparams =
-          (let o,_ = CicEnvironment.get_obj ind_uri CicUniv.empty_ugraph in
+          (let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph ind_uri in
             match o with
                 Cic.Constant _ -> assert false
                | Cic.Variable _ -> assert false