X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_transformations%2Fcontent_expressions.ml;h=65216f5d6a1677ce8f943150601fce54184e720d;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=8c88fd01f1186362a7260c1499c2f56b1eb92fa3;hpb=c5d5bf37b1e4c4b9b499ed2cbfe27cf2ec181944;p=helm.git

diff --git a/helm/ocaml/cic_transformations/content_expressions.ml b/helm/ocaml/cic_transformations/content_expressions.ml
index 8c88fd01f..65216f5d6 100644
--- a/helm/ocaml/cic_transformations/content_expressions.ml
+++ b/helm/ocaml/cic_transformations/content_expressions.ml
@@ -292,11 +292,12 @@ let string_of_sort =
 
 let get_constructors uri i =
   let inductive_types =
-    (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 
     ) in
    let (_,_,_,constructors) = List.nth inductive_types i in
    constructors
@@ -370,7 +371,8 @@ let acic2cexpr ids_to_inner_sorts t =
           make_subst subst, Some uri_str)::List.map acic2cexpr tl)) 
     | C.AAppl (aid,C.AMutInd (sid,uri,i,subst)::tl) ->
         let inductive_types = 
-          (match CicEnvironment.get_obj uri with
+          (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
@@ -398,7 +400,8 @@ let acic2cexpr ids_to_inner_sorts t =
             make_subst subst, Some (UriManager.string_of_uri uri)))
     | C.AMutInd (id,uri,i,subst) ->
         let inductive_types = 
-          (match CicEnvironment.get_obj uri with
+          (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