Added universes handling. The PRE_UNIVERSES tag may help ;)

[helm.git] / helm / ocaml / cic_transformations / acic2Ast.ml

diff --git a/helm/ocaml/cic_transformations/acic2Ast.ml b/helm/ocaml/cic_transformations/acic2Ast.ml
index 567b7f7bb6b38746d1f220251e0362d6d97691e4..d8ded0356fe7de783dfd34942ce4096c2b4e4eb4 100644 (file)
--- a/helm/ocaml/cic_transformations/acic2Ast.ml
+++ b/helm/ocaml/cic_transformations/acic2Ast.ml
@@ -37,11 +37,12 @@ let sort_of_string = function
   | _ -> assert false
 
 let get_types uri =
-  match CicEnvironment.get_obj uri with
-  | Cic.Constant _ -> assert false
-  | Cic.Variable _ -> assert false
-  | Cic.CurrentProof _ -> assert false
-  | Cic.InductiveDefinition (l,_,_) -> l 
+  let o,_ = CicEnvironment.get_obj uri CicUniv.empty_ugraph in
+    match o with
+      | Cic.Constant _ -> assert false
+      | Cic.Variable _ -> assert false
+      | Cic.CurrentProof _ -> assert false
+      | Cic.InductiveDefinition (l,_,_) -> l 
 
 let name_of_inductive_type uri i = 
   let types = get_types uri in