X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fcomponents%2Facic_content%2Facic2content.ml;h=b1423c5ab8cd805670fe4817fcf538c05ebb4107;hb=bcf9a65332d321c25761207e2fb17110dbdc8241;hp=b10464bdad1acd6133dd117709e9221f0be55b12;hpb=cc23f034c9419186602d9250456241f2eba90d7c;p=helm.git

diff --git a/helm/software/components/acic_content/acic2content.ml b/helm/software/components/acic_content/acic2content.ml
index b10464bda..b1423c5ab 100644
--- a/helm/software/components/acic_content/acic2content.ml
+++ b/helm/software/components/acic_content/acic2content.ml
@@ -427,7 +427,7 @@ let rec build_subproofs_and_args ?(headless=false) seed context metasenv l ~ids_
                  if sort = `Prop then 
                     let inductive_types =
                       (let o,_ = 
-			 CicEnvironment.get_obj CicUniv.empty_ugraph uri
+			 CicEnvironment.get_obj CicUniv.oblivion_ugraph uri
 		       in
 			 match o with 
 			   | Cic.InductiveDefinition (l,_,_,_) -> l 
@@ -612,7 +612,7 @@ and acic2content seed context metasenv ?name ~ids_to_inner_sorts ~ids_to_inner_t
         else raise Not_a_proof
     | C.AMutCase (id,uri,typeno,ty,te,patterns) ->
         let inductive_types,noparams =
-          (let o, _ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
+          (let o, _ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in
 	     match o with
 		 Cic.Constant _ -> assert false
                | Cic.Variable _ -> assert false
@@ -780,7 +780,7 @@ and inductive seed context metasenv name id li ~ids_to_inner_types ~ids_to_inner
         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 CicUniv.empty_ugraph ind_uri in
+          (let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph ind_uri in
 	     match o with
                | Cic.InductiveDefinition (l,_,n,_) -> (l,n) 
                | _ -> assert false